Contribution: DescenteInfinie

The Descente Infinie Tactic

Authors

Description

This is a tactic plugin for coq. The tactic helps to prove inductive lemmas by fixpoint functions. A manual for the tactic can be found on its homepage listed above.

Keywords

induction, descente infinie