From 57d83c835edef54c4ead3657aac48c21393c8fb9 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 3 Dec 2024 15:49:08 +1100 Subject: [PATCH] feat: add simp configuration to norm_cast macros --- src/Init/Tactics.lean | 6 +++--- tests/lean/run/norm_cast.lean | 4 ++++ 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 7bb2d6157a..2d35522f1a 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -1318,7 +1318,7 @@ in more situations. Concretely, it runs `norm_cast` on the goal. For each local hypothesis `h`, it also normalizes `h` with `norm_cast` and tries to use that to close the goal. -/ -macro "assumption_mod_cast" : tactic => `(tactic| norm_cast0 at * <;> assumption) +macro "assumption_mod_cast" cfg:optConfig : tactic => `(tactic| norm_cast0 $cfg at * <;> assumption) /-- The `norm_cast` family of tactics is used to normalize certain coercions (*casts*) in expressions. @@ -1355,8 +1355,8 @@ their operation, to make them more flexible about the expressions they accept See also `push_cast`, which moves casts inwards rather than lifting them outwards. -/ -macro "norm_cast" loc:(location)? : tactic => - `(tactic| norm_cast0 $[$loc]? <;> try trivial) +macro "norm_cast" cfg:optConfig loc:(location)? : tactic => + `(tactic| norm_cast0 $cfg $[$loc]? <;> try trivial) /-- diff --git a/tests/lean/run/norm_cast.lean b/tests/lean/run/norm_cast.lean index 56e2b2be39..aa24642a36 100644 --- a/tests/lean/run/norm_cast.lean +++ b/tests/lean/run/norm_cast.lean @@ -85,3 +85,7 @@ theorem b (_h g : true) : true ∧ true := by example : ¬n - k + 1 = 0 := by norm_cast + +/-! Test that we can pass simp configuration options to `norm_cast` -/ +example : ¬n - k + 1 = 0 := by + norm_cast +singlePass