package prooftree

  1. Overview
  2. Docs
Proof-tree visualization for Coq via Proof General

Install

Dune Dependency

askra.de Edit opam file Versions (1)

Authors

  1. H
    Hendrik Tews <hendrik@askra.de>

Maintainers

  1. H
    Hendrik Tews <hendrik@askra.de>

Sources

v0.14.tar.gz
md5=37d1fd23a764191fa3595aca25242357
sha512=a37176d11ed3babad9a67f18da1ba77a2177bceca536fba8b67a9410c1278ce43e85d120c53bd079c686f708257f7df4c309fe258b7b53f56430a4b0f0836965

Description

Prooftree visualizes proof trees during proof development in Coq with Proof General. Prooftree helps against getting lost between different subgoals in interactive proof development. It clearly shows where the current subgoal comes from and thus helps in developing the right plan for solving it.

Published: 27 Feb 2024

Dependencies (4)

  1. lablgtk
  2. coq < "8.17" & >= "8.11"
  3. coq-core >= "8.17"
  4. ocaml >= "4.06"

Dev Dependencies

None

Used by

None

Conflicts

None