|
cctac: congruence-closure for coq
author: Pierre Corbineau,
Stage de DEA au LSV, ENS Cachan
Thèse au LRI, Université Paris Sud XI
Files :
- ccalgo.ml : congruence closure algorithm
- ccproof.ml : proof generation code
- cctac.ml4 : the tactic itself
- CCSolve.v : a small Ltac tactic based on congruence
Known Bugs : the congruence tactic can fail due to type dependencies.
Related documents:
Peter J. Downey, Ravi Sethi, and Robert E. Tarjan.
Variations on the common subexpression problem.
JACM, 27(4):758-771, October 1980.
¤ Dauer der Verarbeitung: 0.4 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
