coq-demos

• 8.5.0
• 8.6.0
• 8.7.0
• 8.8.0

Demos of some Coq tools appeared in version V6.0. Example of sorting algorithms defined using the Cases (pattern-matching) construction. Demo of the decision tactic Tauto for intuitionistic propositional calculus. Demo of the AutoRewrite tactic. Demo of the Prolog tactic applied to the compilation of miniML programs.

opam install coq-demos.8.8.0

homepage

https://github.com/coq-contribs/demos

license

LGPL 2.1

bugs tracker

https://github.com/coq-contribs/demos/issues

dependencies

coq (>= 8.8 & < 8.9~)

source

https://github.com/coq-contribs/demos/archive/v8.8.0.tar.gz

package

https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-demos/coq-demos.8.8.0