Def Lean.MVarId.firstContinuation

Modification history

2023-11-02 05:05
Mathlib/Tactic/Backtrack.lean
feat: patch for std4#196 (more min/max lemmas for `Nat`) (#8074)
Deleted Lean.MVarId.firstContinuationView on Github →
2023-09-13 01:17
Mathlib/Tactic/Backtrack.lean
feat: nondeterminism monad, and use in backtrack (#3464)
Modified Lean.MVarId.firstContinuationView on Github →
2023-04-02 07:27
Mathlib/Tactic/Backtracking.lean
feat: factor out backtracking code from solve_by_elim (#2920) …
Added Lean.MVarId.firstContinuationView on Github →