diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean index 06ebd64ed3..bc8deea42f 100644 --- a/src/Init/Conv.lean +++ b/src/Init/Conv.lean @@ -33,7 +33,7 @@ occurrence of the pattern. syntax occsIndexed := num+ /-- An occurrence specification, either `*` or a list of numbers. The default is `[1]`. -/ -syntax occs := atomic(" (" &"occs") " := " (occsWildcard <|> occsIndexed) ")" +syntax occs := atomic("(" &"occs") " := " (occsWildcard <|> occsIndexed) ") " /-- `with_annotate_state stx t` annotates the lexical range of `stx : Syntax` with diff --git a/src/Lean/Elab/Tactic/Conv/Pattern.lean b/src/Lean/Elab/Tactic/Conv/Pattern.lean index 7f149d6016..c99c617ebf 100644 --- a/src/Lean/Elab/Tactic/Conv/Pattern.lean +++ b/src/Lean/Elab/Tactic/Conv/Pattern.lean @@ -125,7 +125,8 @@ private def pre (pattern : AbstractMVarsResult) (state : IO.Ref PatternMatchStat pure (.occs #[] 0 ids.toList) | _ => throwUnsupportedSyntax let state ← IO.mkRef occs - let (result, _) ← Simp.main lhs (← getContext) (methods := { pre := pre patternA state }) + let ctx := { ← getContext with config.memoize := occs matches .all _ } + let (result, _) ← Simp.main lhs ctx (methods := { pre := pre patternA state }) let subgoals ← match ← state.get with | .all #[] | .occs _ 0 _ => throwError "'pattern' conv tactic failed, pattern was not found{indentExpr patternA.expr}" diff --git a/tests/lean/conv1.lean b/tests/lean/conv1.lean index d90a9575d9..b733c7000e 100644 --- a/tests/lean/conv1.lean +++ b/tests/lean/conv1.lean @@ -245,3 +245,7 @@ example : ((x + y) + z : Nat) = x + (y + z) := by conv => pattern (occs := 1 2 5 macro "bla" : term => `(?a) example : 1 = 1 := by conv => apply bla; congr + +example (h : a = a') (H : a + a' = 0) : a + a = 0 := by + conv in (occs := 2) a => rw [h] + apply H