From 92318d07bb098f01b416bcb43366676b5818c483 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 10 Mar 2022 10:23:18 -0800
Subject: [PATCH] feat: add `MonadBacktrack` instance for
 `CollectPatternVars.M` monad

---
 src/Lean/Elab/PatternVar.lean | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/src/Lean/Elab/PatternVar.lean b/src/Lean/Elab/PatternVar.lean
index 280ff6dd57..cc64ae5b1b 100644
--- a/src/Lean/Elab/PatternVar.lean
+++ b/src/Lean/Elab/PatternVar.lean
@@ -43,9 +43,26 @@ namespace CollectPatternVars
 structure State where
   found     : NameSet := {}
   vars      : Array PatternVar := #[]
+  deriving Inhabited
 
 abbrev M := StateRefT State TermElabM
 
+structure SavedState where
+  term    : Term.SavedState
+  collect : State
+  deriving Inhabited
+
+protected def saveState : M SavedState :=
+  return { term := (← Term.saveState), collect := (← get) }
+
+def SavedState.restore (s : SavedState) (restoreInfo : Bool := false) : M Unit := do
+  s.term.restore restoreInfo
+  set s.collect
+
+instance : MonadBacktrack SavedState M where
+  saveState      := CollectPatternVars.saveState
+  restoreState b := b.restore
+
 private def throwCtorExpected {α} : M α :=
   throwError "invalid pattern, constructor or constant marked with '[matchPattern]' expected"