Sciweavers

ENTCS
2002
95views more  ENTCS 2002»
13 years 4 months ago
A Proof Dedicated Meta-Language
We describe a proof dedicated meta-language, called Ltac, in the context of the Coq proof assistant. This new layer of meta-language is quite appropriate to write small and local ...
David Delahaye