Описание тега ltac
The Ltac language, Coq's domain-specific language for proof search procedures. Use this tag on questions about the language and questions about proof automation using Ltac.
Here are some references on Ltac:
- The Coq Reference Manual, sect. 9;
- Certified Programming with Dependent Types by A. Chlipala, the Proof Search in Ltac chapter;
- The original paper: A Tactic Language for the System Coq by D. Delahaye (2000).