Questions tagged [mizar]
The Mizar system consists of a formal language for writing mathematical definitions and proofs, a proof assistant, which is able to mechanically check proofs written in this language, and a library of formalized mathematics, which can be used in the proof of new theorems. (from Wikipedia)
1
question
10
votes
1
answer
201
views
Is there a Mizar-like sublanguage for Coq?
Isabelle has the frontend Isar which mimics some features of the Mizar system.
I'm curious if Coq has anything similar, i.e. an alternative to tactic scripts that's designed to be readable or similar ...
- 2,671