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

chore: fix tests

Browse Source
This commit is contained in:
Henrik Böving
2026-03-17 10:08:48 +00:00
parent 34a7523611
commit b88612de62
7 changed files with 137 additions and 137 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
tests/elab/Reparen.lean.out.expected
View File

@@ -4029,7 +4029,7 @@ Actions in the resulting monad are functions that take the local value as a para
ordinary actions in `m`.
-/
def ReaderT (ρ : Type u) (m : Type u → Type v) (α : Type u) : Type max u v :=
ρ → m α
(a : @&ρ) → m α
/--
Interpret `ρ → m α` as an element of `ReaderT ρ m α`.

190
tests/elab/attachJp.lean.out.expected
View File

@@ -71,95 +71,95 @@
let _x.4 := Nat.decEq x _x.3;
return _x.4
[Compiler.simp] size: 12
def _private.elab.attachJp.0._eval a.1 a.2 a.3 : EST.Out Lean.Exception lcAny PUnit :=
let _x.4 := "f";
let _x.5 := Lean.Name.mkStr1 _x.4;
let _x.6 := 1;
let _x.7 := @Array.mkEmpty _ _x.6;
let _x.8 := @Array.push _ _x.7 _x.5;
let _x.9 := PUnit.unit;
fun _f.10 _y.11 _y.12 _y.13 _y.14 _y.15 _y.16 _y.17 : EST.Out Lean.Exception lcAny PUnit :=
let _x.18 := Lean.Compiler.compile _x.8 _y.15 _y.16 _y.17;
cases _x.18 : EST.Out Lean.Exception lcAny PUnit
| EST.Out.ok a.19 a.20 =>
let _x.21 := @EST.Out.ok _ _ _ _x.9 a.20;
return _x.21
| EST.Out.error a.22 a.23 =>
return _x.18;
let _x.24 := @Lean.Elab.Command.liftTermElabM _ _f.10 a.1 a.2 a.3;
return _x.24
def _private.elab.attachJp.0._eval @&a @&a a.1 : EST.Out Lean.Exception lcAny PUnit :=
let _x.2 := "f";
let _x.3 := Lean.Name.mkStr1 _x.2;
let _x.4 := 1;
let _x.5 := @Array.mkEmpty _ _x.4;
let _x.6 := @Array.push _ _x.5 _x.3;
let _x.7 := PUnit.unit;
fun _f.8 _y.9 _y.10 _y.11 _y.12 _y.13 _y.14 _y.15 : EST.Out Lean.Exception lcAny PUnit :=
let _x.16 := Lean.Compiler.compile _x.6 _y.13 _y.14 _y.15;
cases _x.16 : EST.Out Lean.Exception lcAny PUnit
| EST.Out.ok a.17 a.18 =>
let _x.19 := @EST.Out.ok _ _ _ _x.7 a.18;
return _x.19
| EST.Out.error a.20 a.21 =>
return _x.16;
let _x.22 := @Lean.Elab.Command.liftTermElabM _ _f.8 a a a.1;
return _x.22
[Compiler.simp] size: 12
def _private.elab.attachJp.0._eval a.1 a.2 a.3 : EST.Out Lean.Exception lcAny PUnit :=
let _x.4 := "f";
let _x.5 := Lean.Name.mkStr1 _x.4;
let _x.6 := 1;
let _x.7 := @Array.mkEmpty _ _x.6;
let _x.8 := @Array.push _ _x.7 _x.5;
let _x.9 := PUnit.unit;
fun _f.10 _y.11 _y.12 _y.13 _y.14 _y.15 _y.16 _y.17 : EST.Out Lean.Exception lcAny PUnit :=
let _x.18 := Lean.Compiler.compile _x.8 _y.15 _y.16 _y.17;
cases _x.18 : EST.Out Lean.Exception lcAny PUnit
| EST.Out.ok a.19 a.20 =>
let _x.21 := @EST.Out.ok _ _ _ _x.9 a.20;
return _x.21
| EST.Out.error a.22 a.23 =>
return _x.18;
let _x.24 := @Lean.Elab.Command.liftTermElabM _ _f.10 a.1 a.2 a.3;
return _x.24
def _private.elab.attachJp.0._eval @&a @&a a.1 : EST.Out Lean.Exception lcAny PUnit :=
let _x.2 := "f";
let _x.3 := Lean.Name.mkStr1 _x.2;
let _x.4 := 1;
let _x.5 := @Array.mkEmpty _ _x.4;
let _x.6 := @Array.push _ _x.5 _x.3;
let _x.7 := PUnit.unit;
fun _f.8 _y.9 _y.10 _y.11 _y.12 _y.13 _y.14 _y.15 : EST.Out Lean.Exception lcAny PUnit :=
let _x.16 := Lean.Compiler.compile _x.6 _y.13 _y.14 _y.15;
cases _x.16 : EST.Out Lean.Exception lcAny PUnit
| EST.Out.ok a.17 a.18 =>
let _x.19 := @EST.Out.ok _ _ _ _x.7 a.18;
return _x.19
| EST.Out.error a.20 a.21 =>
return _x.16;
let _x.22 := @Lean.Elab.Command.liftTermElabM _ _f.8 a a a.1;
return _x.22
[Compiler.simp] size: 12
def _private.elab.attachJp.0._eval a.1 a.2 a.3 : EST.Out Lean.Exception lcAny PUnit :=
let _x.4 := "f";
let _x.5 := Lean.Name.mkStr1 _x.4;
let _x.6 := 1;
let _x.7 := @Array.mkEmpty _ _x.6;
let _x.8 := @Array.push _ _x.7 _x.5;
let _x.9 := PUnit.unit;
fun _f.10 _y.11 _y.12 _y.13 _y.14 _y.15 _y.16 _y.17 : EST.Out Lean.Exception lcAny PUnit :=
let _x.18 := Lean.Compiler.compile _x.8 _y.15 _y.16 _y.17;
cases _x.18 : EST.Out Lean.Exception lcAny PUnit
| EST.Out.ok a.19 a.20 =>
let _x.21 := @EST.Out.ok _ _ _ _x.9 a.20;
return _x.21
| EST.Out.error a.22 a.23 =>
return _x.18;
let _x.24 := @Lean.Elab.Command.liftTermElabM _ _f.10 a.1 a.2 a.3;
return _x.24
def _private.elab.attachJp.0._eval @&a @&a a.1 : EST.Out Lean.Exception lcAny PUnit :=
let _x.2 := "f";
let _x.3 := Lean.Name.mkStr1 _x.2;
let _x.4 := 1;
let _x.5 := @Array.mkEmpty _ _x.4;
let _x.6 := @Array.push _ _x.5 _x.3;
let _x.7 := PUnit.unit;
fun _f.8 _y.9 _y.10 _y.11 _y.12 _y.13 _y.14 _y.15 : EST.Out Lean.Exception lcAny PUnit :=
let _x.16 := Lean.Compiler.compile _x.6 _y.13 _y.14 _y.15;
cases _x.16 : EST.Out Lean.Exception lcAny PUnit
| EST.Out.ok a.17 a.18 =>
let _x.19 := @EST.Out.ok _ _ _ _x.7 a.18;
return _x.19
| EST.Out.error a.20 a.21 =>
return _x.16;
let _x.22 := @Lean.Elab.Command.liftTermElabM _ _f.8 a a a.1;
return _x.22
[Compiler.simp] size: 12
def _private.elab.attachJp.0._eval a.1 a.2 a.3 : EST.Out Lean.Exception lcAny PUnit :=
let _x.4 := "f";
let _x.5 := Lean.Name.mkStr1 _x.4;
let _x.6 := 1;
let _x.7 := Array.mkEmpty ◾ _x.6;
let _x.8 := Array.push ◾ _x.7 _x.5;
let _x.9 := PUnit.unit;
fun _f.10 _y.11 _y.12 _y.13 _y.14 _y.15 _y.16 _y.17 : EST.Out Lean.Exception lcAny PUnit :=
let _x.18 := Lean.Compiler.compile _x.8 _y.15 _y.16 _y.17;
cases _x.18 : EST.Out Lean.Exception lcAny PUnit
| EST.Out.ok a.19 a.20 =>
let _x.21 := @EST.Out.ok ◾ ◾ ◾ _x.9 a.20;
return _x.21
| EST.Out.error a.22 a.23 =>
return _x.18;
let _x.24 := Lean.Elab.Command.liftTermElabM._redArg _f.10 a.1 a.2 a.3;
return _x.24
def _private.elab.attachJp.0._eval @&a @&a a.1 : EST.Out Lean.Exception lcAny PUnit :=
let _x.2 := "f";
let _x.3 := Lean.Name.mkStr1 _x.2;
let _x.4 := 1;
let _x.5 := Array.mkEmpty ◾ _x.4;
let _x.6 := Array.push ◾ _x.5 _x.3;
let _x.7 := PUnit.unit;
fun _f.8 _y.9 _y.10 _y.11 _y.12 _y.13 _y.14 _y.15 : EST.Out Lean.Exception lcAny PUnit :=
let _x.16 := Lean.Compiler.compile _x.6 _y.13 _y.14 _y.15;
cases _x.16 : EST.Out Lean.Exception lcAny PUnit
| EST.Out.ok a.17 a.18 =>
let _x.19 := @EST.Out.ok ◾ ◾ ◾ _x.7 a.18;
return _x.19
| EST.Out.error a.20 a.21 =>
return _x.16;
let _x.22 := Lean.Elab.Command.liftTermElabM._redArg _f.8 a a a.1;
return _x.22
[Compiler.simp] size: 12
def _private.elab.attachJp.0._eval a.1 a.2 a.3 : EST.Out Lean.Exception lcAny PUnit :=
let _x.4 := "f";
let _x.5 := Lean.Name.mkStr1 _x.4;
let _x.6 := 1;
let _x.7 := Array.mkEmpty ◾ _x.6;
let _x.8 := Array.push ◾ _x.7 _x.5;
let _x.9 := PUnit.unit;
fun _f.10 _y.11 _y.12 _y.13 _y.14 _y.15 _y.16 _y.17 : EST.Out Lean.Exception lcAny PUnit :=
let _x.18 := Lean.Compiler.compile _x.8 _y.15 _y.16 _y.17;
cases _x.18 : EST.Out Lean.Exception lcAny PUnit
| EST.Out.ok a.19 a.20 =>
let _x.21 := @EST.Out.ok ◾ ◾ ◾ _x.9 a.20;
return _x.21
| EST.Out.error a.22 a.23 =>
return _x.18;
let _x.24 := Lean.Elab.Command.liftTermElabM._redArg _f.10 a.1 a.2 a.3;
return _x.24
def _private.elab.attachJp.0._eval @&a @&a a.1 : EST.Out Lean.Exception lcAny PUnit :=
let _x.2 := "f";
let _x.3 := Lean.Name.mkStr1 _x.2;
let _x.4 := 1;
let _x.5 := Array.mkEmpty ◾ _x.4;
let _x.6 := Array.push ◾ _x.5 _x.3;
let _x.7 := PUnit.unit;
fun _f.8 _y.9 _y.10 _y.11 _y.12 _y.13 _y.14 _y.15 : EST.Out Lean.Exception lcAny PUnit :=
let _x.16 := Lean.Compiler.compile _x.6 _y.13 _y.14 _y.15;
cases _x.16 : EST.Out Lean.Exception lcAny PUnit
| EST.Out.ok a.17 a.18 =>
let _x.19 := @EST.Out.ok ◾ ◾ ◾ _x.7 a.18;
return _x.19
| EST.Out.error a.20 a.21 =>
return _x.16;
let _x.22 := Lean.Elab.Command.liftTermElabM._redArg _f.8 a a a.1;
return _x.22
[Compiler.simp] size: 5
def _private.elab.attachJp.0._eval._lam_0 _x.1 _x.2 _y.3 _y.4 _y.5 _y.6 _y.7 _y.8 _y.9 : EST.Out Lean.Exception
lcAny PUnit :=
@@ -171,13 +171,13 @@
| EST.Out.error a.14 a.15 =>
return _x.10
[Compiler.simp] size: 8
def _private.elab.attachJp.0._eval a.1 a.2 a.3 : EST.Out Lean.Exception lcAny PUnit :=
let _x.4 := "f";
let _x.5 := Lean.Name.mkStr1 _x.4;
let _x.6 := 1;
let _x.7 := Array.mkEmpty ◾ _x.6;
let _x.8 := Array.push ◾ _x.7 _x.5;
let _x.9 := PUnit.unit;
let _f.10 := _eval._lam_0 _x.8 _x.9;
let _x.11 := Lean.Elab.Command.liftTermElabM._redArg _f.10 a.1 a.2 a.3;
return _x.11
def _private.elab.attachJp.0._eval @&a @&a a.1 : EST.Out Lean.Exception lcAny PUnit :=
let _x.2 := "f";
let _x.3 := Lean.Name.mkStr1 _x.2;
let _x.4 := 1;
let _x.5 := Array.mkEmpty ◾ _x.4;
let _x.6 := Array.push ◾ _x.5 _x.3;
let _x.7 := PUnit.unit;
let _f.8 := _eval._lam_0 _x.6 _x.7;
let _x.9 := Lean.Elab.Command.liftTermElabM._redArg _f.8 a a a.1;
return _x.9

18
tests/elab/casesOnSameCtor.lean
View File

@@ -146,15 +146,15 @@ trace: [Compiler.saveMono] size: 5
| EST.Out.error a.15 a.16 =>
return _x.11
[Compiler.saveMono] size: 7
def _private.elab.casesOnSameCtor.0._eval a.1 a.2 a.3 : EST.Out Exception lcAny PUnit :=
let _x.4 := "List";
let _x.5 := "match_on_same_ctor";
let _x.6 := Name.mkStr2 _x.4 _x.5;
let _x.7 := Name.mkStr1 _x.4;
let _x.8 := PUnit.unit;
let _f.9 := _eval._lam_0 _x.6 _x.7 _x.8;
let _x.10 := Lean.Elab.Command.liftTermElabM._redArg _f.9 a.1 a.2 a.3;
return _x.10
def _private.elab.casesOnSameCtor.0._eval @&a @&a a.1 : EST.Out Exception lcAny PUnit :=
let _x.2 := "List";
let _x.3 := "match_on_same_ctor";
let _x.4 := Name.mkStr2 _x.2 _x.3;
let _x.5 := Name.mkStr1 _x.2;
let _x.6 := PUnit.unit;
let _f.7 := _eval._lam_0 _x.4 _x.5 _x.6;
let _x.8 := Lean.Elab.Command.liftTermElabM._redArg _f.7 a a a.1;
return _x.8
-/
#guard_msgs in
set_option trace.Compiler.saveMono true in

20
tests/elab/emptyLcnf.lean
View File

@@ -22,16 +22,16 @@ trace: [Compiler.saveMono] size: 5
| EST.Out.error a.14 a.15 =>
return _x.10
[Compiler.saveMono] size: 8
def _private.elab.emptyLcnf.0._eval a.1 a.2 a.3 : EST.Out Lean.Exception lcAny PUnit :=
let _x.4 := "f";
let _x.5 := Lean.Name.mkStr1 _x.4;
let _x.6 := 1;
let _x.7 := Array.mkEmpty ◾ _x.6;
let _x.8 := Array.push ◾ _x.7 _x.5;
let _x.9 := PUnit.unit;
let _f.10 := _eval._lam_0 _x.8 _x.9;
let _x.11 := Lean.Elab.Command.liftTermElabM._redArg _f.10 a.1 a.2 a.3;
return _x.11
def _private.elab.emptyLcnf.0._eval @&a @&a a.1 : EST.Out Lean.Exception lcAny PUnit :=
let _x.2 := "f";
let _x.3 := Lean.Name.mkStr1 _x.2;
let _x.4 := 1;
let _x.5 := Array.mkEmpty ◾ _x.4;
let _x.6 := Array.push ◾ _x.5 _x.3;
let _x.7 := PUnit.unit;
let _f.8 := _eval._lam_0 _x.6 _x.7;
let _x.9 := Lean.Elab.Command.liftTermElabM._redArg _f.8 a a a.1;
return _x.9
-/
#guard_msgs in
run_meta Lean.Compiler.compile #[``f]

24
tests/elab/erased.lean
View File

@@ -37,21 +37,21 @@ trace: [Compiler.saveMono] size: 5
| EST.Out.error (a.14 : Lean.Exception) (a.15 : lcVoid) =>
return _x.10
[Compiler.saveMono] size: 9
def _private.elab.erased.0._eval (a.1 : Lean.Elab.Command.Context) (a.2 : lcAny) (a.3 : lcVoid) : EST.Out
def _private.elab.erased.0._eval (a : @&Lean.Elab.Command.Context) (a : @&lcAny) (a.1 : lcVoid) : EST.Out
Lean.Exception lcAny PUnit :=
let _x.4 : String := "Erased";
let _x.5 : String := "mk";
let _x.6 : Lean.Name := Lean.Name.mkStr2 _x.4 _x.5;
let _x.7 : Nat := 1;
let _x.8 : Array Lean.Name := Array.mkEmpty ◾ _x.7;
let _x.9 : Array Lean.Name := Array.push ◾ _x.8 _x.6;
let _x.10 : PUnit := PUnit.unit;
let _f.11 : Lean.Elab.Term.Context →
let _x.2 : String := "Erased";
let _x.3 : String := "mk";
let _x.4 : Lean.Name := Lean.Name.mkStr2 _x.2 _x.3;
let _x.5 : Nat := 1;
let _x.6 : Array Lean.Name := Array.mkEmpty ◾ _x.5;
let _x.7 : Array Lean.Name := Array.push ◾ _x.6 _x.4;
let _x.8 : PUnit := PUnit.unit;
let _f.9 : Lean.Elab.Term.Context →
lcAny →
Lean.Meta.Context →
lcAny → Lean.Core.Context → lcAny → lcVoid → EST.Out Lean.Exception lcAny PUnit := _eval._lam_0 _x.9 _x.10;
let _x.12 : EST.Out Lean.Exception lcAny PUnit := Lean.Elab.Command.liftTermElabM._redArg _f.11 a.1 a.2 a.3;
return _x.12
lcAny → Lean.Core.Context → lcAny → lcVoid → EST.Out Lean.Exception lcAny PUnit := _eval._lam_0 _x.7 _x.8;
let _x.10 : EST.Out Lean.Exception lcAny PUnit := Lean.Elab.Command.liftTermElabM._redArg _f.9 a a a.1;
return _x.10
-/
#guard_msgs in
run_meta Lean.Compiler.compile #[``Erased.mk]

18
tests/elab/inlineApp.lean
View File

@@ -25,15 +25,15 @@ trace: [Compiler.saveMono] size: 1
let _x.9 := Lean.Compiler.compile _x.1 _y.6 _y.7 _y.8;
return _x.9
[Compiler.saveMono] size: 7
def _private.elab.inlineApp.0._eval a.1 a.2 a.3 : EST.Out Lean.Exception lcAny PUnit :=
let _x.4 := "h";
let _x.5 := Lean.Name.mkStr1 _x.4;
let _x.6 := 1;
let _x.7 := Array.mkEmpty ◾ _x.6;
let _x.8 := Array.push ◾ _x.7 _x.5;
let _f.9 := _eval._lam_0 _x.8;
let _x.10 := Lean.Elab.Command.liftTermElabM._redArg _f.9 a.1 a.2 a.3;
return _x.10
def _private.elab.inlineApp.0._eval @&a @&a a.1 : EST.Out Lean.Exception lcAny PUnit :=
let _x.2 := "h";
let _x.3 := Lean.Name.mkStr1 _x.2;
let _x.4 := 1;
let _x.5 := Array.mkEmpty ◾ _x.4;
let _x.6 := Array.push ◾ _x.5 _x.3;
let _f.7 := _eval._lam_0 _x.6;
let _x.8 := Lean.Elab.Command.liftTermElabM._redArg _f.7 a a a.1;
return _x.8
-/
#guard_msgs in
set_option trace.Compiler.saveMono true in

2
tests/elab/meta6.lean.out.expected
View File

@@ -1,7 +1,7 @@
[Meta.debug] ----- tst2 -----
[Meta.debug] #[a, b, motive, t, inl, inr]
[Meta.debug] #[a, b, motive, intro, t]
[Meta.debug] #[x, a._@._internal._hyg.0, a._@._internal._hyg.0, a._@._internal._hyg.0, a._@._internal._hyg.0, a._@._internal._hyg.0]
[Meta.debug] #[x, a, a, a, a, a._@._internal._hyg.0]
[Meta.debug] @False.elim.{0}
(@GT.gt.{0} Nat instLTNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))
(@OfNat.ofNat.{0} Nat (nat_lit 5) (instOfNatNat (nat_lit 5))))