search

jonsterling / racket-grit

Grit: the kernel around which a PRL forms
Other
3 stars 0 forks source link

higher order proof refinement #9

Closed jonsterling closed 7 years ago

jonsterling commented 7 years ago

I've got the syntax (and macros) worked out for defining higher order proof refinement rules, which is pretty sweet...

The next step is to implement the refinement engine, which will execute compositions of these rules in the form of tactics.

Furthermore, I would like to generalize the framework to handle n-ary outputs/extracts, but we have to think a little bit about how to do that.

david-christiansen commented 7 years ago

Isn't this taken care of now, except perhaps for the last bit?

jonsterling commented 7 years ago

yes, i think we can close this one... I'll open a new ticket for multiple outputs.