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.

Estimated changes