search

proofpeer / proofpeer-proofscript

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

Implement operators on theorems and terms #10

Closed phlegmaticprogrammer closed 10 years ago

phlegmaticprogrammer commented 10 years ago

There are a few operators that need to be implemented to expose all of the proof methods of Context at the ProofScript level. Also stuff like term equality needs to be implemented, not sure if that should be only modulo alpha, or also modulo beta/eta conversion.