proofpeer / proofpeer-proofscript

The language of ProofPeer: ProofScript
MIT License
8 stars 0 forks source link

Add theory assumes check. #11

Closed phlegmaticprogrammer closed 10 years ago

phlegmaticprogrammer commented 10 years ago

Except for the theory \root, no theory should be allowed to introduce toplevel assumes. That way, each theory is a conservative extension of theory \root