MMode A Mizar Mode for the proof assistant Coq. Abstract. We present a set of tactics for version 7.4 of the Coq proof assistant which makes it possible to write proofs for Coq in a language similar to the proof language of the Mizar system. These tactics can be used with any interface of Coq, and they can be freely mixed with the normal Coq tactics.
Keywords for this software
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- Korniłowicz, Artur: Flexary connectives in Mizar (2015)
- Pąk, Karol: Improving legibility of formal proofs based on the close reference principle is NP-hard (2015)
- Pąk, Karol: Improving legibility of natural deduction proofs is not trivial (2014)