Skip to content
Sections
>> Trisquel >> Packages >> etiona >> science >> prooftree
etiona  ] [  nabia  ] [  aramo  ]
[ Source: prooftree  ]

Package: prooftree (0.13-1build3)

proof-tree visualization for Proof General

Prooftree draws proof trees during interactive proof development with Proof General. One can inspect goals and proof commands and check where existential variables were introduced and instantiated. Currently, Prooftree does only work for Coq.

Other Packages Related to prooftree

  • depends
  • recommends
  • suggests
  • dep: coq (>= 8.4)
    proof assistant for higher-order logic (toplevel and compiler)
  • dep: libc6 (>= 2.17)
    GNU C Library: Shared libraries
    also a virtual package provided by libc6-udeb
  • dep: libgdk-pixbuf2.0-0 (>= 2.22.0)
    GDK Pixbuf library
  • dep: libglib2.0-0 (>= 2.35.9)
    GLib library of C routines
  • dep: libgtk2.0-0 (>= 2.24.31)
    GTK+ graphical user interface library
  • dep: libpango-1.0-0 (>= 1.14.0)
    Layout and rendering of internationalized text
  • dep: proofgeneral (>= 4.3~pre130510)
    generic frontend for proof assistants

Download prooftree

Download for all available architectures
Architecture Package Size Installed Size Files
amd64 812.1 kB4231 kB [list of files]
i386 732.5 kB3426 kB [list of files]