Contribution: Demos
Demos of some Coq tools appeared in version V6.0
Authors
- Coq group
Description
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.
Keywords
sorting, cases, tauto, autorewrite, prolog