issues
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
WF tactic improvements
#207
Closed
jonsterling
closed
9 years ago
jonsterling
commented
9 years ago
Adds a
wf-lemma <my-lemma>
tactic that automates some annoying backchaining stuff
Adds a
wf
resource, and calls it during
Auto
wf-lemma <my-lemma>
tactic that automates some annoying backchaining stuffwf
resource, and calls it duringAuto