search

jonsterling / JonPRL

An proof refinement logic for computational type theory. Inspired by Nuprl. [For up-to-date development, see JonPRL's successor, RedPRL: https://github.com/redprl/sml-redprl]
http://www.jonprl.org
MIT License
109 stars 9 forks source link

Canonical-forms tests #222

Open jonsterling opened 8 years ago

jonsterling commented 8 years ago

I'd like to add canonical-forms tests like Nuprl has... But rather than adding one for each canonical operator, it would be cool to do it all at once, as in match-operator{θ}(M; L; R), where the parameter θ is a canonical operator. This expression only has a value in case θ is known to be a canonical operator.

The operational semantics would be:

  match-operator{θ}(θ(...); L; R)  :-> L    (θ can)
  match-operator{θ}(θ'(...); L; R) :-> R    (θ can)
  match-operator{θ}(_; _; _)       :-> _|_  (θ non-can)