A Proof Dedicated Meta-Language
David Delahaye · Electronic Notes in Theoretical Computer Science · 2002
We describe a proof dedicated meta-language, called L tac, in the context of the Coq proof assistant. This new layer of meta-language is quite appropriate to write small and local automations. L tac, is essentially a small functional core with recursors and powerful pattern-matching operators for Coq terms but also for proof contexts. As L tac, is not complete, we describe an interface between L tac, and the full programmable meta-language of the system (Objective CAML), which is also the implementation language. This interface is based on a quotation system where we can use L tac,'s syntax in ML files, and where it is possible to insert ML code in L tac, scripts by means of antiquotations. In that way, the two meta-languages are not opposed and we give an example where they fairly cooperate. Thus, this shows that a LCF-like system with a two-level meta-language is completely realistic.