wip, added tactic to narrow state, tactic to register new lemma

openai / lean-gym

Apache License 2.0

150 stars 31 forks source link

Closed Scikud closed 2 years ago

Scikud commented 2 years ago

WIP added tactics to narrow state to conjecture, register new lemma given prf expr.