adc45d7c7b
This PR marks any exposed (non-private) auxiliary match declaration as `[implicit_reducible]`. This is essential when the outer declaration is marked as `instance_reducible` — without it, reduction is blocked at the match auxiliary. We do not inherit the attribute from the parent declaration because match auxiliary declarations are reused across definitions, and the reducibility setting of the parent can change independently. This change prepares for implementing the TODO at `ExprDefEq.lean:465`, which would otherwise cause too many failures requiring manual `[implicit_reducible]` annotations on match declarations whose names are not necessarily derived from the outer function. --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
40 lines
1.1 KiB
Text
40 lines
1.1 KiB
Text
def f : Nat → Nat
|
|
| 0 => 0
|
|
| 10 => 1
|
|
| 100 => 2
|
|
| _ => 3
|
|
|
|
|
|
/--
|
|
info: @[implicit_reducible] def f.match_1.{u_1} : (motive : Nat → Sort u_1) →
|
|
(x : Nat) → (Unit → motive 0) → (Unit → motive 10) → (Unit → motive 100) → ((x : Nat) → motive x) → motive x
|
|
-/
|
|
#guard_msgs in
|
|
#print sig f.match_1
|
|
|
|
|
|
/--
|
|
info: private def f.match_1.splitter.{u_1} : (motive : Nat → Sort u_1) →
|
|
(x : Nat) →
|
|
(Unit → motive 0) →
|
|
(Unit → motive 10) →
|
|
(Unit → motive 100) → ((x : Nat) → (x = 0 → False) → (x = 10 → False) → (x = 100 → False) → motive x) → motive x
|
|
-/
|
|
#guard_msgs in
|
|
#print sig f.match_1.splitter
|
|
|
|
/--
|
|
info: private theorem f.match_1.eq_4.{u_1} : ∀ (motive : Nat → Sort u_1) (x : Nat) (h_1 : Unit → motive 0)
|
|
(h_2 : Unit → motive 10) (h_3 : Unit → motive 100) (h_4 : (x : Nat) → motive x),
|
|
(x = 0 → False) →
|
|
(x = 10 → False) →
|
|
(x = 100 → False) →
|
|
(match x with
|
|
| 0 => h_1 ()
|
|
| 10 => h_2 ()
|
|
| 100 => h_3 ()
|
|
| x => h_4 x) =
|
|
h_4 x
|
|
-/
|
|
#guard_msgs in
|
|
#print sig f.match_1.eq_4
|