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

Fix functionality bug; change per type arity #244

Closed jonsterling closed 8 years ago

jonsterling commented 8 years ago

Thanks to @vrahli for putting this together. I'm opening the PR so that we have a more central way to discuss the changes. Summary:

  1. Vincent has fixed #243. That's what happens when we just guess what a rule should be! :) In Nuprl, if you browse through the rules, you will see only CallLisp for this one, since it is not possible to express a variadic rule in Nuprl's rule calculus.
  2. Vincent has resolved #241 (switching the per operator to have arity (exp,exp.exp)exp instead of (exp)exp). This is mostly a cosmetic change.
  3. Vincent has added the Pointwise Functionality rule, which can be very useful.
  4. I have fixed the proof that CTT is predicative (russell.jonprl). Vincent has fixed the halting problem proof. I've disabled some of the proofs in the synthetic topology development until I understand better how to reproduce them.
jonsterling commented 8 years ago

I'm going to merge this now, since I think it's working pretty well and I have a demo tomorrow.