factor out a MetaM tactic

wellecks / llmstep

llmstep: [L]LM proofstep suggestions in Lean 4.

MIT License

118 stars 15 forks source link

Closed kim-em closed 1 year ago

kim-em commented 1 year ago

Minor refactor to pull out a MetaM level tactic, that could be used in e.g. proof search.

wellecks commented 1 year ago

💯