sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

test: update expected output for beta-reduced delayed assignments

Browse Source 
instantiateAllMVars resolves delayed assignments by substituting fvars
inline rather than constructing (fun x => body) arg beta-redexes, producing
more beta-reduced (but definitionally equal) terms.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
This commit is contained in:
Joachim Breitner
2026-03-04 08:39:12 +00:00
parent bc0324b381
commit 81deb0a369
2 changed files with 32 additions and 35 deletions
Download Patch File Download Diff File Expand all files Collapse all files

22
tests/elab/1179b.lean.out.expected
View File

@@ -2,15 +2,13 @@ def Foo.bar.match_1.{u_1} : {l₂ : Nat} →
(motive : Foo l₂ → Sort u_1) →
(t₂ : Foo l₂) → ((s₁ : Foo l₂) → motive s₁.cons) → ((x : Foo l₂) → motive x) → motive t₂ :=
fun {l₂} motive t₂ h_1 h_2 =>
(fun t₂_1 =>
Foo.bar._sparseCasesOn_1 (motive := fun a x => l₂ = a → t₂ ≍ x → motive t₂) t₂_1
(fun {l} t h =>
Eq.ndrec (motive := fun {l} => (t : Foo l) → t₂ ≍ t.cons → motive t₂)
(fun t h => Eq.symm (eq_of_heq h) ▸ h_1 t) h t)
fun h h_3 =>
Eq.ndrec (motive := fun a => (t₂_2 : Foo a) → Nat.hasNotBit 2 t₂_2.ctorIdx → t₂ ≍ t₂_2 → motive t₂)
(fun t₂_2 h h_4 =>
Eq.ndrec (motive := fun t₂_3 => Nat.hasNotBit 2 t₂_3.ctorIdx → motive t₂) (fun h => h_2 t₂) (eq_of_heq h_4)
h)
h_3 t₂_1 h)
t₂ (Eq.refl l₂) (HEq.refl t₂)
Foo.bar._sparseCasesOn_1 (motive := fun a x => l₂ = a → t₂ ≍ x → motive t₂) t₂
(fun {l} t h =>
Eq.ndrec (motive := fun {l} => (t : Foo l) → t₂ ≍ t.cons → motive t₂) (fun t h => Eq.symm (eq_of_heq h) ▸ h_1 t) h
t)
(fun h h_3 =>
Eq.ndrec (motive := fun a => (t₂_1 : Foo a) → Nat.hasNotBit 2 t₂_1.ctorIdx → t₂ ≍ t₂_1 → motive t₂)
(fun t₂_1 h h_4 =>
Eq.ndrec (motive := fun t₂_2 => Nat.hasNotBit 2 t₂_2.ctorIdx → motive t₂) (fun h => h_2 t₂) (eq_of_heq h_4) h)
h_3 t₂ h)
(Eq.refl l₂) (HEq.refl t₂)

45
tests/elab/depElim1.lean.out.expected
View File

@@ -24,29 +24,28 @@ def elimTest2.{u_1, u_2} : (α : Type u_1) →
(x : α) → (xs : Vec α n) → (y : α) → (ys : Vec α n) → motive (n + 1) (Vec.cons x xs) (Vec.cons y ys)) →
motive n xs ys :=
fun α motive n xs ys h_1 h_2 =>
(fun xs_1 =>
Vec.casesOn (motive := fun a x => n = a → xs ≍ x → motive n xs ys) xs_1
(fun h =>
Eq.ndrec (motive := fun n => (xs ys : Vec α n) → xs ≍ Vec.nil → motive n xs ys)
(fun xs ys h =>
⋯ ▸
Vec.casesOn (motive := fun a x => 0 = a → ys ≍ x → motive 0 Vec.nil ys) ys (fun h h_3 => ⋯ ▸ h_1 ())
(fun {n} a a_1 h => False.elim ⋯) ⋯ ⋯)
⋯ xs ys)
fun {n_1} a a_1 h =>
Eq.ndrec (motive := fun n => (xs ys : Vec α n) → xs ≍ Vec.cons a a_1 → motive n xs ys)
(fun xs ys h =>
⋯ ▸
Vec.casesOn (motive := fun a_2 x => n_1 + 1 = a_2 → ys ≍ x → motive (n_1 + 1) (Vec.cons a a_1) ys) ys
(fun h => False.elim ⋯)
(fun {n} a_2 a_3 h =>
n_1.elimOffset n 1 h fun x =>
Eq.ndrec (motive := fun {n} =>
(a_4 : Vec α n) → ys ≍ Vec.cons a_2 a_4 → motive (n_1 + 1) (Vec.cons a a_1) ys)
(fun a_4 h => ⋯ ▸ h_2 n_1 a a_1 a_2 a_4) x a_3)
⋯ ⋯)
⋯ xs ys)
xs ⋯ ⋯
Vec.casesOn (motive := fun a x => n = a → xs ≍ x → motive n xs ys) xs
(fun h =>
Eq.ndrec (motive := fun n => (xs ys : Vec α n) → xs ≍ Vec.nil → motive n xs ys)
(fun xs ys h =>
⋯ ▸
Vec.casesOn (motive := fun a x => 0 = a → ys ≍ x → motive 0 Vec.nil ys) ys (fun h h_3 => ⋯ ▸ h_1 ())
(fun {n} a a_1 h => False.elim ⋯) ⋯ ⋯)
⋯ xs ys)
(fun {n_1} a a_1 h =>
Eq.ndrec (motive := fun n => (xs ys : Vec α n) → xs ≍ Vec.cons a a_1 → motive n xs ys)
(fun xs ys h =>
⋯ ▸
Vec.casesOn (motive := fun a_2 x => n_1 + 1 = a_2 → ys ≍ x → motive (n_1 + 1) (Vec.cons a a_1) ys) ys
(fun h => False.elim ⋯)
(fun {n} a_2 a_3 h =>
n_1.elimOffset n 1 h fun x =>
Eq.ndrec (motive := fun {n} =>
(a_4 : Vec α n) → ys ≍ Vec.cons a_2 a_4 → motive (n_1 + 1) (Vec.cons a a_1) ys)
(fun a_4 h => ⋯ ▸ h_2 n_1 a a_1 a_2 a_4) x a_3)
⋯ ⋯)
⋯ xs ys)
⋯ ⋯
elimTest3 : forall (α : Type.{u_1}) (β : Type.{u_2}) (motive : (List.{u_1} α) -> (List.{u_2} β) -> Sort.{u_3}) (x : List.{u_1} α) (y : List.{u_2} β), (Unit -> (motive (List.nil.{u_1} α) (List.nil.{u_2} β))) -> (forall (a : α) (b : β), motive (List.cons.{u_1} α a (List.nil.{u_1} α)) (List.cons.{u_2} β b (List.nil.{u_2} β))) -> (forall (a₁ : α) (a₂ : α) (as : List.{u_1} α) (b₁ : β) (b₂ : β) (bs : List.{u_2} β), motive (List.cons.{u_1} α a₁ (List.cons.{u_1} α a₂ as)) (List.cons.{u_2} β b₁ (List.cons.{u_2} β b₂ bs))) -> (forall (as : List.{u_1} α) (bs : List.{u_2} β), motive as bs) -> (motive x y)
def elimTest3.{u_1, u_2, u_3} : (α : Type u_1) →
(β : Type u_2) →