Commit 2023-03-16 19:28 6a3ed56f
View on Github →feat: port clear_value
tactic (#2916)
Copies the structure of the clear
tactic and Lean.MVarId.changeLocalDecl
to implement the clear_value
tactic.
feat: port clear_value
tactic (#2916)
Copies the structure of the clear
tactic and Lean.MVarId.changeLocalDecl
to implement the clear_value
tactic.