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.