Skip to content

Commit 6fd84dc

Browse files
committed
fix tests
1 parent 707542e commit 6fd84dc

File tree

2 files changed

+33
-32
lines changed

2 files changed

+33
-32
lines changed

tests/lean/run/emptyLcnf.lean

Lines changed: 15 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,8 @@ trace: [Compiler.result] size: 0
1212
1313
---
1414
trace: [Compiler.result] size: 5
15-
def _eval._lam_0 _x.1 _x.2 _y.3 _y.4 _y.5 _y.6 _y.7 _y.8 _y.9 : EStateM.Result Lean.Exception lcRealWorld PUnit :=
15+
def _private.lean.run.emptyLcnf.0._eval._lam_0 _x.1 _x.2 _y.3 _y.4 _y.5 _y.6 _y.7 _y.8 _y.9 : EStateM.Result
16+
Lean.Exception lcRealWorld PUnit :=
1617
let _x.10 := Lean.Compiler.compile _x.1 _y.7 _y.8 _y.9;
1718
cases _x.10 : EStateM.Result Lean.Exception lcRealWorld PUnit
1819
| EStateM.Result.ok a.11 a.12 =>
@@ -21,34 +22,34 @@ trace: [Compiler.result] size: 5
2122
| EStateM.Result.error a.14 a.15 =>
2223
return _x.10
2324
[Compiler.result] size: 1
24-
def _eval._closed_0 : String :=
25+
def _private.lean.run.emptyLcnf.0._eval._closed_0 : String :=
2526
let _x.1 := "f";
2627
return _x.1
2728
[Compiler.result] size: 2
28-
def _eval._closed_1 : Lean.Name :=
29-
let _x.1 := _eval._closed_0;
29+
def _private.lean.run.emptyLcnf.0._eval._closed_1 : Lean.Name :=
30+
let _x.1 := _eval._closed_0.2;
3031
let _x.2 := Lean.Name.mkStr1 _x.1;
3132
return _x.2
3233
[Compiler.result] size: 2
33-
def _eval._closed_2 : Array Lean.Name :=
34+
def _private.lean.run.emptyLcnf.0._eval._closed_2 : Array Lean.Name :=
3435
let _x.1 := 1;
3536
let _x.2 := Array.mkEmpty ◾ _x.1;
3637
return _x.2
3738
[Compiler.result] size: 3
38-
def _eval._closed_3 : Array Lean.Name :=
39-
let _x.1 := _eval._closed_1;
40-
let _x.2 := _eval._closed_2;
39+
def _private.lean.run.emptyLcnf.0._eval._closed_3 : Array Lean.Name :=
40+
let _x.1 := _eval._closed_1.2;
41+
let _x.2 := _eval._closed_2.2;
4142
let _x.3 := Array.push ◾ _x.2 _x.1;
4243
return _x.3
4344
[Compiler.result] size: 8
44-
def _eval a.1 a.2 a.3 : EStateM.Result Lean.Exception lcRealWorld PUnit :=
45-
let _x.4 := _eval._closed_0;
46-
let _x.5 := _eval._closed_1;
45+
def _private.lean.run.emptyLcnf.0._eval a.1 a.2 a.3 : EStateM.Result Lean.Exception lcRealWorld PUnit :=
46+
let _x.4 := _eval._closed_0.2;
47+
let _x.5 := _eval._closed_1.2;
4748
let _x.6 := 1;
48-
let _x.7 := _eval._closed_2;
49-
let _x.8 := _eval._closed_3;
49+
let _x.7 := _eval._closed_2.2;
50+
let _x.8 := _eval._closed_3.2;
5051
let _x.9 := PUnit.unit;
51-
let _f.10 := _eval._lam_0 _x.8 _x.9;
52+
let _f.10 := _eval._lam_0.2 _x.8 _x.9;
5253
let _x.11 := Lean.Elab.Command.liftTermElabM._redArg _f.10 a.1 a.2 a.3;
5354
return _x.11
5455
-/

tests/lean/run/erased.lean

Lines changed: 18 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ trace: [Compiler.result] size: 1
2626
return _x.1
2727
---
2828
trace: [Compiler.result] size: 5
29-
def _eval._lam_0 (_x.1 : Array
29+
def _private.lean.run.erased.0._eval._lam_0 (_x.1 : Array
3030
Lean.Name) (_x.2 : PUnit) (_y.3 : Lean.Elab.Term.Context) (_y.4 : lcAny) (_y.5 : Lean.Meta.Context) (_y.6 : lcAny) (_y.7 : Lean.Core.Context) (_y.8 : lcAny) (_y.9 : lcRealWorld) : EStateM.Result
3131
Lean.Exception lcRealWorld PUnit :=
3232
let _x.10 : EStateM.Result Lean.Exception lcRealWorld PUnit := compile _x.1 _y.7 _y.8 _y.9;
@@ -37,46 +37,46 @@ trace: [Compiler.result] size: 5
3737
| EStateM.Result.error (a.14 : Lean.Exception) (a.15 : lcRealWorld) =>
3838
return _x.10
3939
[Compiler.result] size: 1
40-
def _eval._closed_0 : String :=
40+
def _private.lean.run.erased.0._eval._closed_0 : String :=
4141
let _x.1 : String := "Erased";
4242
return _x.1
4343
[Compiler.result] size: 1
44-
def _eval._closed_1 : String :=
44+
def _private.lean.run.erased.0._eval._closed_1 : String :=
4545
let _x.1 : String := "mk";
4646
return _x.1
4747
[Compiler.result] size: 3
48-
def _eval._closed_2 : Lean.Name :=
49-
let _x.1 : String := _eval._closed_1;
50-
let _x.2 : String := _eval._closed_0;
48+
def _private.lean.run.erased.0._eval._closed_2 : Lean.Name :=
49+
let _x.1 : String := _eval._closed_1.2;
50+
let _x.2 : String := _eval._closed_0.2;
5151
let _x.3 : Lean.Name := Lean.Name.mkStr2 _x.2 _x.1;
5252
return _x.3
5353
[Compiler.result] size: 2
54-
def _eval._closed_3 : Array Lean.Name :=
54+
def _private.lean.run.erased.0._eval._closed_3 : Array Lean.Name :=
5555
let _x.1 : Nat := 1;
5656
let _x.2 : Array Lean.Name := Array.mkEmpty ◾ _x.1;
5757
return _x.2
5858
[Compiler.result] size: 3
59-
def _eval._closed_4 : Array Lean.Name :=
60-
let _x.1 : Lean.Name := _eval._closed_2;
61-
let _x.2 : Array Lean.Name := _eval._closed_3;
59+
def _private.lean.run.erased.0._eval._closed_4 : Array Lean.Name :=
60+
let _x.1 : Lean.Name := _eval._closed_2.2;
61+
let _x.2 : Array Lean.Name := _eval._closed_3.2;
6262
let _x.3 : Array Lean.Name := Array.push ◾ _x.2 _x.1;
6363
return _x.3
6464
[Compiler.result] size: 9
65-
def _eval (a.1 : Lean.Elab.Command.Context) (a.2 : lcAny) (a.3 : lcRealWorld) : EStateM.Result Lean.Exception
66-
lcRealWorld PUnit :=
67-
let _x.4 : String := _eval._closed_0;
68-
let _x.5 : String := _eval._closed_1;
69-
let _x.6 : Lean.Name := _eval._closed_2;
65+
def _private.lean.run.erased.0._eval (a.1 : Lean.Elab.Command.Context) (a.2 : lcAny) (a.3 : lcRealWorld) : EStateM.Result
66+
Lean.Exception lcRealWorld PUnit :=
67+
let _x.4 : String := _eval._closed_0.2;
68+
let _x.5 : String := _eval._closed_1.2;
69+
let _x.6 : Lean.Name := _eval._closed_2.2;
7070
let _x.7 : Nat := 1;
71-
let _x.8 : Array Lean.Name := _eval._closed_3;
72-
let _x.9 : Array Lean.Name := _eval._closed_4;
71+
let _x.8 : Array Lean.Name := _eval._closed_3.2;
72+
let _x.9 : Array Lean.Name := _eval._closed_4.2;
7373
let _x.10 : PUnit := PUnit.unit;
7474
let _f.11 : Lean.Elab.Term.Context →
7575
lcAny →
7676
Lean.Meta.Context →
7777
lcAny →
7878
Lean.Core.Context →
79-
lcAny → lcRealWorld → EStateM.Result Lean.Exception lcRealWorld PUnit := _eval._lam_0 _x.9 _x.10;
79+
lcAny → lcRealWorld → EStateM.Result Lean.Exception lcRealWorld PUnit := _eval._lam_0.2 _x.9 _x.10;
8080
let _x.12 : EStateM.Result Lean.Exception lcRealWorld
8181
PUnit := Lean.Elab.Command.liftTermElabM._redArg _f.11 a.1 a.2 a.3;
8282
return _x.12

0 commit comments

Comments
 (0)