Fully support types - Githubissues

proofpeer / proofpeer-proofscript

The language of ProofPeer: ProofScript

MIT License

8 stars 0 forks source link

Fully support types #49

Closed phlegmaticprogrammer closed 9 years ago

phlegmaticprogrammer commented 9 years ago

Types are currently treated as second class citizen in ProofScript, they appear only as part of terms. There is a need to have full first-order support for types, in particular:

a ProofScript datatype representing a type
composing and decomposing types
pattern matching for types

phlegmaticprogrammer commented 9 years ago

I've added full support for types, see /scripts/issues/issues49.thy for syntax & semantics.