Lean Kernel Arena / lazylean

Version: 0.3.0 · 📄 Declaration · 🔗 Source

Test "bugs/constlevels"

Expected: ✋ reject · Size: 15.3 KB · Lines: 283 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Test result: ✋ rejected · exit code 1 · wall time: 56 ms · instructions: 8.0 M · max rss memory: 21.6 MB

stderr:

loaded 12 declarations, 204 exprs (204 unique), 63 names in 0.000346058s
declaration order verified in 2.575e-06s
environment built in 3.3052e-05s; checking with 4 worker processes
FAIL _test (line 283): let value type mismatch for 'x'
checked 11 declarations, 1 failed, in 0.00293292s wall (2.27176e-06 core-hours over 4 workers); 4 reduction steps; peak 20 MB in one worker

Test "bugs/ctor-num-fields"

Expected: ✋ reject · Size: 34.1 KB · Lines: 622 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 16 ms · instructions: 8.3 M · max rss memory: 22.0 MB

stderr:

loaded 25 declarations, 465 exprs (465 unique), 124 names in 0.000254997s
declaration order verified in 5.039e-06s
environment built in 2.0659e-05s; checking with 4 worker processes
FAIL _private.Test.0.S (line 235): constructor field/parameter/index counts do not match: _private.Test.0.S.mk
checked 7 declarations, 1 failed, in 0.00310107s wall (2.0987e-06 core-hours over 4 workers); 2 reduction steps; peak 20 MB in one worker

Test "bugs/eta-ctor-alias"

Expected: ✋ reject · Size: 7.2 KB · Lines: 122 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 16 ms · instructions: 7.1 M · max rss memory: 21.7 MB

stderr:

loaded 5 declarations, 85 exprs (85 unique), 28 names in 0.000189274s
declaration order verified in 7.363e-06s
environment built in 1.5149e-05s; checking with 4 worker processes
FAIL etaCtorAlias (line 122): declaration type mismatch for 'etaCtorAlias'
  inferred: ((a : BoxFn) -> (((Eq.{1} BoxFn) #0) #0))
  declared: ((f : BoxFn) -> (((Eq.{1} BoxFn) #0) Box.mk))
checked 4 declarations, 1 failed, in 0.00209027s wall (1.39533e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "bugs/k-rec-conv"

Expected: ✋ reject · Size: 12.6 KB · Lines: 232 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 15 ms · instructions: 7.9 M · max rss memory: 21.7 MB

stderr:

loaded 9 declarations, 158 exprs (158 unique), 60 names in 0.000217397s
declaration order verified in 2.515e-06s
environment built in 1.9627e-05s; checking with 4 worker processes
FAIL bad (line 232): declaration type mismatch for 'bad'
  inferred: (((Eq.{1} T) t1) t1)
  declared: (((Eq.{1} T) t1) t2)
checked 8 declarations, 1 failed, in 0.00266411s wall (1.9099e-06 core-hours over 4 workers); 3 reduction steps; peak 20 MB in one worker

Test "bugs/large-elim-param"

Expected: ✋ reject · Size: 6.2 KB · Lines: 88 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

inductive MyBool.{u} : Sort u | tt | ff

Test result: ✋ rejected · exit code 1 · wall time: 14 ms · instructions: 7.1 M · max rss memory: 21.8 MB

stderr:

loaded 5 declarations, 58 exprs (58 unique), 21 names in 0.00016564s
declaration order verified in 2.184e-06s
environment built in 1.6411e-05s; checking with 4 worker processes
FAIL MyBool (line 86): recursor 'MyBool.rec' should only eliminate into Prop
checked 3 declarations, 1 failed, in 0.00162661s wall (1.18232e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "bugs/large-elim-prop-bool"

Expected: ✋ reject · Size: 22.6 KB · Lines: 438 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 15 ms · instructions: 8.1 M · max rss memory: 21.7 MB

stderr:

loaded 17 declarations, 318 exprs (318 unique), 95 names in 0.000317093s
declaration order verified in 3.146e-06s
environment built in 1.9937e-05s; checking with 4 worker processes
FAIL NewBool (line 307): recursor 'NewBool.rec' should only eliminate into Prop
checked 8 declarations, 1 failed, in 0.0025424s wall (1.94229e-06 core-hours over 4 workers); 28 reduction steps; peak 20 MB in one worker

Test "bugs/level-imax-leq"

Expected: ✋ reject · Size: 5.6 KB · Lines: 93 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Test result: ✋ rejected · exit code 1 · wall time: 13 ms · instructions: 6.7 M · max rss memory: 21.7 MB

stderr:

loaded 5 declarations, 59 exprs (59 unique), 22 names in 0.000113132s
declaration order verified in 1.963e-06s
environment built in 1.4076e-05s; checking with 4 worker processes
FAIL False (line 69): recursor 'False.rec' elimination universe is named 'u_1', expected 'u'
checked 0 declarations, 1 failed, in 0.00126034s wall (7.39964e-07 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "bugs/level-imax-normalization"

Expected: ✋ reject · Size: 5.8 KB · Lines: 96 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Test result: ✋ rejected · exit code 1 · wall time: 12 ms · instructions: 7.0 M · max rss memory: 21.8 MB

stderr:

loaded 6 declarations, 60 exprs (60 unique), 24 names in 0.000119013s
declaration order verified in 2.154e-06s
environment built in 1.4958e-05s; checking with 4 worker processes
FAIL down (line 77): declaration type mismatch for 'down'
  inferred: ((x : Sort((imax 0 v)+1)) -> Sort((imax 0 v)+1))
  declared: ((x : Sort((imax 0 v)+1)) -> Sort((imax 0 v)))
checked 5 declarations, 1 failed, in 0.00154847s wall (9.2406e-07 core-hours over 4 workers); 22 reduction steps; peak 19 MB in one worker

Test "bugs/nat-rec-k-lie"

Expected: ✋ reject · Size: 6.3 KB · Lines: 106 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Test result: ✋ rejected · exit code 1 · wall time: 12 ms · instructions: 6.8 M · max rss memory: 22.0 MB

stderr:

loaded 6 declarations, 67 exprs (67 unique), 30 names in 0.000121648s
declaration order verified in 2.154e-06s
environment built in 1.5109e-05s; checking with 4 worker processes
FAIL Nat (line 59): recursor 'Nat.rec': parameter/index/motive/minor/K data differs from the derived recursor
checked 2 declarations, 1 failed, in 0.00119514s wall (8.13924e-07 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "bugs/nat-rec-rules"

Expected: ✋ reject · Size: 8.1 KB · Lines: 128 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Test result: ✋ rejected · exit code 1 · wall time: 16 ms · instructions: 6.9 M · max rss memory: 21.9 MB

stderr:

loaded 6 declarations, 92 exprs (92 unique), 27 names in 0.000228979s
declaration order verified in 3.336e-06s
environment built in 1.8675e-05s; checking with 4 worker processes
FAIL False (line 91): recursor 'False.rec' elimination universe is named 'u_1', expected 'u'
checked 0 declarations, 1 failed, in 0.00261844s wall (1.58067e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "bugs/nested-unused-param"

Expected: ✋ reject · Size: 61.1 KB · Lines: 1.1 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 20 ms · instructions: 14.5 M · max rss memory: 22.3 MB

stderr:

loaded 38 declarations, 826 exprs (826 unique), 208 names in 0.000511057s
declaration order verified in 6.483e-06s
environment built in 5.8801e-05s; checking with 4 worker processes
FAIL e (line 1048): invalid projection C.0
FAIL E (line 1036): invalid projection C.0
checked 33 declarations, 2 failed, in 0.00586346s wall (5.10621e-06 core-hours over 4 workers); 436 reduction steps; peak 22 MB in one worker

Test "bugs/orphan-rec"

Expected: ✋ reject · Size: 1.4 KB · Lines: 21 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Test result: ✋ rejected · exit code 1 · wall time: 14 ms · instructions: 6.4 M · max rss memory: 21.8 MB

stderr:

loaded 2 declarations, 10 exprs (10 unique), 7 names in 0.000100448s
declaration order verified in 2.895e-06s
environment built in 1.6852e-05s; checking with 4 worker processes
FAIL False (line 18): recursor count mismatch for 'False': export has 2, derived 1
checked 0 declarations, 1 failed, in 0.00160308s wall (1.0179e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "bugs/proj-non-structure"

Expected: ✋ reject · Size: 5.0 KB · Lines: 75 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 16 ms · instructions: 6.8 M · max rss memory: 21.9 MB

stderr:

loaded 4 declarations, 48 exprs (48 unique), 21 names in 0.000142507s
declaration order verified in 3.988e-06s
environment built in 1.5979e-05s; checking with 4 worker processes
FAIL bad (line 75): invalid projection Bad.0
checked 3 declarations, 1 failed, in 0.00222876s wall (1.42149e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "bugs/proj-of-imax-prop"

Expected: ✋ reject · Size: 19.3 KB · Lines: 321 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 16 ms · instructions: 7.9 M · max rss memory: 21.6 MB

stderr:

loaded 19 declarations, 217 exprs (217 unique), 80 names in 0.000175229s
declaration order verified in 2.615e-06s
environment built in 1.9627e-05s; checking with 4 worker processes
FAIL imaxProjBool (line 245): invalid projection ImaxProp.0
checked 12 declarations, 1 failed, in 0.00235681s wall (1.689e-06 core-hours over 4 workers); 6 reduction steps; peak 20 MB in one worker

Test "bugs/proj-of-stuck-prop"

Expected: ✋ reject · Size: 275.7 KB · Lines: 5.3 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 23 ms · instructions: 52.3 M · max rss memory: 26.1 MB

stderr:

loaded 120 declarations, 4367 exprs (4367 unique), 755 names in 0.000797073s
declaration order verified in 1.9426e-05s
environment built in 4.9383e-05s; checking with 4 worker processes
FAIL Native64ResultSort.asProp (line 4735): application type mismatch in ((id.{1} Sort(0)) ((Native64ResultSortOwner $0) $2))
  argument type: ((((((((Native64ResultSortGate.rec.{2} $0) (fun (index : Bool) => (fun (index : Bool) => (fun (index : Bool) => (fun (index : Bool) => (fun (proof : (((((Native64ResultSortGate $0) #3) #2) #1) #0)) => Sort(1))))))) Sort(0)) (Native64SortGateB.0.3766726852 ((fun (salt : Nat) => $0) (((OfNat.ofNat.{0} Nat) 125330) (instOfNatNat 125330))))) (Native64SortGateA.1.2023879994 ((fun (salt : Nat) => $0) (((OfNat.ofNat.{0} Nat) 125330) (instOfNatNat 125330))))) (Native64SortGateA.1.2023879994 ((fun (salt : Nat) => $0) (((OfNat.ofNat.{0} Nat) 125330) (instOfNatNat 125330))))) (Native64SortGateA.1.2023879994 ((fun (salt : Nat) => $0) (((OfNat.ofNat.{0} Nat) 125330) (instOfNatNat 125330))))) $2)
  expected: Sort(0)
FAIL Native64ResultSortOwner (line 4727): type expected: ((((((((Native64ResultSortGate.rec.{2} $8) (fun (index : Bool) => (fun (index : Bool) => (fun (index : Bool) => (fun (index : Bool) => (fun (proof : (((((Native64ResultSortGate $8) #3) #2) #1) #0)) => Sort(1))))))) Sort(0)) (Native64SortGateB.0.3766726852 ((fun (salt : Nat) => $8) (((OfNat.ofNat.{0} Nat) 125330) (instOfNatNat 125330))))) (Native64SortGateA.1.2023879994 ((fun (salt : Nat) => $8) (((OfNat.ofNat.{0} Nat) 125330) (instOfNatNat 125330))))) (Native64SortGateA.1.2023879994 ((fun (salt : Nat) => $8) (((OfNat.ofNat.{0} Nat) 125330) (instOfNatNat 125330))))) (Native64SortGateA.1.2023879994 ((fun (salt : Nat) => $8) (((OfNat.ofNat.{0} Nat) 125330) (instOfNatNat 125330))))) $9)
checked 105 declarations, 2 failed, in 0.00893658s wall (8.53098e-06 core-hours over 4 workers); 1587 reduction steps; peak 26 MB in one worker

Test "bugs/proj-of-subst-prop"

Expected: ✋ reject · Size: 254.9 KB · Lines: 4.8 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 21 ms · instructions: 55.6 M · max rss memory: 23.7 MB

stderr:

loaded 113 declarations, 4004 exprs (4004 unique), 712 names in 0.000858698s
declaration order verified in 2.112e-05s
environment built in 4.5796e-05s; checking with 4 worker processes
FAIL PR14806Subst.observe (line 4827): type expected: (PR14806Subst.Owner PR14806Subst.witness)
checked 111 declarations, 1 failed, in 0.00845755s wall (8.09633e-06 core-hours over 4 workers); 2405 reduction steps; peak 23 MB in one worker

Test "bugs/rec-k-lie"

Expected: ✋ reject · Size: 5.3 KB · Lines: 87 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 16 ms · instructions: 6.7 M · max rss memory: 21.7 MB

stderr:

loaded 5 declarations, 49 exprs (49 unique), 30 names in 0.000109244s
declaration order verified in 2.375e-06s
environment built in 1.4547e-05s; checking with 4 worker processes
FAIL MyBool (line 35): recursor 'MyBool.rec': parameter/index/motive/minor/K data differs from the derived recursor
checked 1 declarations, 1 failed, in 0.00192472s wall (9.65068e-07 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "bugs/rec-missing-ih"

Expected: ✋ reject · Size: 289.6 KB · Lines: 5.5 k · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Test result: ✋ rejected · exit code 1 · wall time: 21 ms · instructions: 54.9 M · max rss memory: 23.7 MB

stderr:

loaded 118 declarations, 4596 exprs (4596 unique), 793 names in 0.000662852s
declaration order verified in 1.2493e-05s
environment built in 3.8682e-05s; checking with 4 worker processes
FAIL Native64TwoHashOwner (line 4811): arg #3 of 'Native64TwoHashOwner.step' has a non valid occurrence of the datatypes being declared
checked 108 declarations, 1 failed, in 0.00865516s wall (7.70263e-06 core-hours over 4 workers); 1754 reduction steps; peak 23 MB in one worker

Test "bugs/rec-of-subst-prop"

Expected: ✋ reject · Size: 269.2 KB · Lines: 5.1 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 21 ms · instructions: 55.3 M · max rss memory: 23.6 MB

stderr:

loaded 130 declarations, 4165 exprs (4165 unique), 780 names in 0.000840894s
declaration order verified in 1.6832e-05s
environment built in 4.9463e-05s; checking with 4 worker processes
FAIL Issue.opaqueEndpoint (line 4760): declaration type mismatch for 'Issue.opaqueEndpoint'
  inferred: ((p : Issue.ModeP) -> (((Eq.{1} Nat) ((Nat.add (Issue.modeG Issue.modeQ)) 0)) ((Nat.add (Issue.modeG Issue.modeQ)) 0)))
  declared: ((p : Issue.ModeP) -> (((Eq.{1} Nat) ((Nat.add (Issue.modeG #0)) 0)) ((Nat.add (Issue.modeG Issue.modeQ)) 0)))
checked 116 declarations, 1 failed, in 0.00956853s wall (9.01795e-06 core-hours over 4 workers); 2279 reduction steps; peak 23 MB in one worker

Test "cedar"

Expected: 👍 accept · Size: 832.0 MB · Lines: 15.3 M · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 24.1 s · instructions: 461.0 G · max rss memory: 1015.4 MB

stderr:

loaded 143203 declarations, 14152792 exprs (14152792 unique), 1019732 names in 2.36305s
declaration order verified in 0.114353s
environment built in 0.0646236s; checking with 4 worker processes
checked 143203 declarations, 0 failed, in 21.5997s wall (0.0239544 core-hours over 4 workers); 90538782 reduction steps; peak 1015 MB in one worker

Test "con-leche"

Expected: 👍 accept · Size: 525.9 MB · Lines: 10.0 M · lean4export: 3.1.0 · Lean: 4.33.0 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 28.6 s · instructions: 456.7 G · max rss memory: 617.3 MB

stderr:

loaded 26819 declarations, 9679077 exprs (9679077 unique), 337090 names in 1.75534s
declaration order verified in 0.106542s
environment built in 0.0107156s; checking with 4 worker processes
checked 26819 declarations, 0 failed, in 26.8222s wall (0.0292153 core-hours over 4 workers); 79091265 reduction steps; peak 617 MB in one worker

Test "corner-cases/alg-conv-trans-acc"

Expected: 🤷 either · Size: 66.4 KB · Lines: 1.2 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 22 ms · instructions: 17.6 M · max rss memory: 23.0 MB

stderr:

loaded 40 declarations, 920 exprs (920 unique), 200 names in 0.000413887s
declaration order verified in 7.284e-06s
environment built in 2.8644e-05s; checking with 4 worker processes
FAIL trans (line 1176): declaration type mismatch for 'trans'
  inferred: ((a : (((Acc.{1} Nat) (fun (x1._@.Test.1043551373._hygCtx._hyg.6 : Nat) => (fun (x2._@.Test.1043551373._hygCtx._hyg.6 : Nat) => ((((LT.lt.{0} Nat) instLTNat) #1) #0)))) (((OfNat.ofNat.{0} Nat) 1) (instOfNatNat 1)))) -> (((Eq.{1} Bool) ((f (((OfNat.ofNat.{0} Nat) 1) (instOfNatNat 1))) #0)) ((f (((OfNat.ofNat.{0} Nat) 1) (instOfNatNat 1))) #0)))
  declared: ((a : (((Acc.{1} Nat) (fun (x1._@.Test.1043551373._hygCtx._hyg.6 : Nat) => (fun (x2._@.Test.1043551373._hygCtx._hyg.6 : Nat) => ((((LT.lt.{0} Nat) instLTNat) #1) #0)))) (((OfNat.ofNat.{0} Nat) 1) (instOfNatNat 1)))) -> (((Eq.{1} Bool) ((f (((OfNat.ofNat.{0} Nat) 1) (instOfNatNat 1))) #0)) ((f (((OfNat.ofNat.{0} Nat) 0) (instOfNatNat 0))) ((((((Acc.inv.{1} Nat) (fun (x1._@.Test.1043551373._hygCtx._hyg.6 : Nat) => (fun (x2._@.Test.1043551373._hygCtx._hyg.6 : Nat) => ((((LT.lt.{0} Nat) instLTNat) #1) #0)))) (((OfNat.ofNat.{0} Nat) 1) (instOfNatNat 1))) (((OfNat.ofNat.{0} Nat) 0) (instOfNatNat 0))) #0) (Nat.lt_succ_self (((OfNat.ofNat.{0} Nat) 0) (instOfNatNat 0)))))))
checked 39 declarations, 1 failed, in 0.0064774s wall (5.85821e-06 core-hours over 4 workers); 488 reduction steps; peak 22 MB in one worker

Test "corner-cases/alg-conv-trans-acc-left"

Expected: 🤷 either · Size: 67.4 KB · Lines: 1.2 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 18 ms · instructions: 17.4 M · max rss memory: 22.4 MB

stderr:

loaded 41 declarations, 934 exprs (934 unique), 205 names in 0.000329198s
declaration order verified in 7.515e-06s
environment built in 2.8864e-05s; checking with 4 worker processes
checked 41 declarations, 0 failed, in 0.00570179s wall (5.11178e-06 core-hours over 4 workers); 502 reduction steps; peak 22 MB in one worker

Test "corner-cases/alg-conv-trans-acc-right"

Expected: 🤷 either · Size: 67.6 KB · Lines: 1.2 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 21 ms · instructions: 17.9 M · max rss memory: 22.3 MB

stderr:

loaded 41 declarations, 941 exprs (941 unique), 205 names in 0.000345408s
declaration order verified in 5.941e-06s
environment built in 2.6169e-05s; checking with 4 worker processes
checked 41 declarations, 0 failed, in 0.00646081s wall (5.84234e-06 core-hours over 4 workers); 639 reduction steps; peak 22 MB in one worker

Test "corner-cases/alg-conv-trans-quot"

Expected: 🤷 either · Size: 8.5 KB · Lines: 169 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 18 ms · instructions: 7.3 M · max rss memory: 21.7 MB

stderr:

loaded 6 declarations, 127 exprs (127 unique), 31 names in 0.000145062s
declaration order verified in 2.365e-06s
environment built in 1.7923e-05s; checking with 4 worker processes
FAIL trans (line 169): declaration type mismatch for 'trans'
  inferred: ((P : Sort(0)) -> ((r : ((a._@._internal._hyg.0 : #0) -> ((a._@._internal._hyg.0 : #1) -> Sort(0)))) -> ((α : Sort(1)) -> ((f : ((a : #2) -> #1)) -> ((h : ((x : #3) -> ((y : #4) -> ((a._@._internal._hyg.0 : ((#4 #1) #0)) -> (((Eq.{1} #4) (#3 #2)) (#3 #1)))))) -> ((q : ((Quot.{0} #4) #3)) -> ((z : #5) -> (((Eq.{1} #4) ((((((Quot.lift.{0, 1} #6) #5) #4) #3) #2) #1)) ((((((Quot.lift.{0, 1} #6) #5) #4) #3) #2) #1)))))))))
  declared: ((P : Sort(0)) -> ((r : ((a._@._internal._hyg.0 : #0) -> ((a._@._internal._hyg.0 : #1) -> Sort(0)))) -> ((α : Sort(1)) -> ((f : ((a : #2) -> #1)) -> ((h : ((x : #3) -> ((y : #4) -> ((a._@._internal._hyg.0 : ((#4 #1) #0)) -> (((Eq.{1} #4) (#3 #2)) (#3 #1)))))) -> ((q : ((Quot.{0} #4) #3)) -> ((z : #5) -> (((Eq.{1} #4) ((((((Quot.lift.{0, 1} #6) #5) #4) #3) #2) #1)) (#3 #0)))))))))
checked 5 declarations, 1 failed, in 0.00341123s wall (1.91529e-06 core-hours over 4 workers); 0 reduction steps; peak 21 MB in one worker

Test "corner-cases/alg-conv-trans-quot-left"

Expected: 🤷 either · Size: 8.6 KB · Lines: 173 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 19 ms · instructions: 7.3 M · max rss memory: 21.6 MB

stderr:

loaded 6 declarations, 131 exprs (131 unique), 31 names in 0.000117941s
declaration order verified in 2.765e-06s
environment built in 1.8565e-05s; checking with 4 worker processes
FAIL left (line 173): declaration type mismatch for 'left'
  inferred: ((P : Sort(0)) -> ((r : ((a._@._internal._hyg.0 : #0) -> ((a._@._internal._hyg.0 : #1) -> Sort(0)))) -> ((α : Sort(1)) -> ((f : ((a : #2) -> #1)) -> ((h : ((x : #3) -> ((y : #4) -> ((a._@._internal._hyg.0 : ((#4 #1) #0)) -> (((Eq.{1} #4) (#3 #2)) (#3 #1)))))) -> ((q : ((Quot.{0} #4) #3)) -> ((z : #5) -> (((Eq.{1} #4) ((((((Quot.lift.{0, 1} #6) #5) #4) #3) #2) #1)) ((((((Quot.lift.{0, 1} #6) #5) #4) #3) #2) #1)))))))))
  declared: ((P : Sort(0)) -> ((r : ((a._@._internal._hyg.0 : #0) -> ((a._@._internal._hyg.0 : #1) -> Sort(0)))) -> ((α : Sort(1)) -> ((f : ((a : #2) -> #1)) -> ((h : ((x : #3) -> ((y : #4) -> ((a._@._internal._hyg.0 : ((#4 #1) #0)) -> (((Eq.{1} #4) (#3 #2)) (#3 #1)))))) -> ((q : ((Quot.{0} #4) #3)) -> ((z : #5) -> (((Eq.{1} #4) ((((((Quot.lift.{0, 1} #6) #5) #4) #3) #2) #1)) ((((((Quot.lift.{0, 1} #6) #5) #4) #3) #2) (((Quot.mk.{0} #6) #5) #0))))))))))
checked 5 declarations, 1 failed, in 0.00351612s wall (1.95107e-06 core-hours over 4 workers); 0 reduction steps; peak 21 MB in one worker

Test "corner-cases/alg-conv-trans-quot-left-def"

Expected: 🤷 either · Size: 10.5 KB · Lines: 208 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 19 ms · instructions: 7.4 M · max rss memory: 21.6 MB

stderr:

loaded 8 declarations, 160 exprs (160 unique), 34 names in 0.000236584s
declaration order verified in 6.472e-06s
environment built in 2.2612e-05s; checking with 4 worker processes
checked 8 declarations, 0 failed, in 0.00431429s wall (2.39063e-06 core-hours over 4 workers); 0 reduction steps; peak 20 MB in one worker

Test "corner-cases/alg-conv-trans-quot-right"

Expected: 🤷 either · Size: 9.0 KB · Lines: 180 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 21 ms · instructions: 7.2 M · max rss memory: 21.7 MB

stderr:

loaded 7 declarations, 136 exprs (136 unique), 32 names in 0.00020773s
declaration order verified in 2.815e-06s
environment built in 1.6702e-05s; checking with 4 worker processes
checked 7 declarations, 0 failed, in 0.00413702s wall (1.96978e-06 core-hours over 4 workers); 2 reduction steps; peak 20 MB in one worker

Test "corner-cases/eta-ctor"

Expected: 🤷 either · Size: 9.0 KB · Lines: 148 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 16 ms · instructions: 7.2 M · max rss memory: 21.7 MB

stderr:

loaded 6 declarations, 104 exprs (104 unique), 34 names in 0.000174869s
declaration order verified in 2.375e-06s
environment built in 1.5689e-05s; checking with 4 worker processes
FAIL etaCtor (line 148): declaration type mismatch for 'etaCtor'
  inferred: ((a : ((proof : True) -> T)) -> (((Eq.{1} ((proof : True) -> T)) #0) #0))
  declared: ((x : ((proof : True) -> T)) -> (((Eq.{1} ((proof : True) -> T)) (T.mk (T.val (#0 True.intro)))) #0))
checked 5 declarations, 1 failed, in 0.00276466s wall (1.79659e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "corner-cases/eta-rec-struct"

Expected: 🤷 either · Size: 9.5 KB · Lines: 174 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 17 ms · instructions: 7.4 M · max rss memory: 21.6 MB

stderr:

loaded 4 declarations, 124 exprs (124 unique), 38 names in 0.000201869s
declaration order verified in 3.426e-06s
environment built in 1.9186e-05s; checking with 4 worker processes
FAIL etaRecStruct (line 174): declaration type mismatch for 'etaRecStruct'
  inferred: ((a : ((a._@._internal._hyg.0 : ((Prod.{0, 0} Bool) Bool)) -> Bool)) -> (((Eq.{1} ((a._@._internal._hyg.0 : ((Prod.{0, 0} Bool) Bool)) -> Bool)) #0) #0))
  declared: ((a : ((a._@._internal._hyg.0 : ((Prod.{0, 0} Bool) Bool)) -> Bool)) -> (((Eq.{1} ((a._@._internal._hyg.0 : ((Prod.{0, 0} Bool) Bool)) -> Bool)) ((((Prod.rec.{1, 0, 0} Bool) Bool) (fun (x._@.Test.3091511195._hygCtx._hyg.21 : ((Prod.{0, 0} Bool) Bool)) => Bool)) (fun (b : Bool) => (fun (c : Bool) => (#2 ((((Prod.mk.{0, 0} Bool) Bool) #1) #0)))))) #0))
checked 3 declarations, 1 failed, in 0.00336147s wall (2.50781e-06 core-hours over 4 workers); 0 reduction steps; peak 20 MB in one worker

Test "corner-cases/eta-rule-k"

Expected: 🤷 either · Size: 6.5 KB · Lines: 121 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 19 ms · instructions: 7.1 M · max rss memory: 21.9 MB

stderr:

loaded 3 declarations, 85 exprs (85 unique), 29 names in 0.000230172s
declaration order verified in 6.082e-06s
environment built in 2.0559e-05s; checking with 4 worker processes
FAIL etaRuleK (line 121): declaration type mismatch for 'etaRuleK'
  inferred: ((a : ((a._@._internal._hyg.0 : (((Eq.{1} Bool) Bool.true) Bool.true)) -> Bool)) -> (((Eq.{1} ((a._@._internal._hyg.0 : (((Eq.{1} Bool) Bool.true) Bool.true)) -> Bool)) #0) #0))
  declared: ((a : ((a._@._internal._hyg.0 : (((Eq.{1} Bool) Bool.true) Bool.true)) -> Bool)) -> (((Eq.{1} ((a._@._internal._hyg.0 : (((Eq.{1} Bool) Bool.true) Bool.true)) -> Bool)) (((((Eq.rec.{1, 1} Bool) Bool.true) (fun (x._@.Test.1420384072._hygCtx._hyg.30 : Bool) => (fun (x._@.Test.1420384072._hygCtx._hyg.32 : (((Eq.{1} Bool) Bool.true) #0)) => Bool))) (#0 ((Eq.refl.{1} Bool) Bool.true))) Bool.true)) #0))
checked 2 declarations, 1 failed, in 0.00340591s wall (2.04228e-06 core-hours over 4 workers); 0 reduction steps; peak 20 MB in one worker

Test "corner-cases/eta-struct-major-and"

Expected: 🤷 either · Size: 9.4 KB · Lines: 175 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 19 ms · instructions: 7.6 M · max rss memory: 21.6 MB

stderr:

loaded 5 declarations, 130 exprs (130 unique), 36 names in 0.000220574s
declaration order verified in 2.224e-06s
environment built in 2.2803e-05s; checking with 4 worker processes
FAIL andMajorEta (line 175): declaration type mismatch for 'andMajorEta'
  inferred: ((P : Sort(0)) -> ((Q : Sort(0)) -> ((A : Sort(1)) -> ((f : ((a._@._internal._hyg.0 : #2) -> ((a._@._internal._hyg.0 : #2) -> #2))) -> ((x : ((And #3) #2)) -> (((Eq.{1} #2) (((((And.rec.{1} #4) #3) (fun (x._@.Test.3893811644._hygCtx._hyg.27 : ((And #4) #3)) => #3)) #1) #0)) (((((And.rec.{1} #4) #3) (fun (x._@.Test.3893811644._hygCtx._hyg.27 : ((And #4) #3)) => #3)) #1) #0)))))))
  declared: ((P : Sort(0)) -> ((Q : Sort(0)) -> ((A : Sort(1)) -> ((f : ((a._@._internal._hyg.0 : #2) -> ((a._@._internal._hyg.0 : #2) -> #2))) -> ((x : ((And #3) #2)) -> (((Eq.{1} #2) (((((And.rec.{1} #4) #3) (fun (x._@.Test.3893811644._hygCtx._hyg.27 : ((And #4) #3)) => #3)) #1) ((((And.intro #4) #3) (((And.left #4) #3) #0)) (((And.right #4) #3) #0)))) (((((And.rec.{1} #4) #3) (fun (x._@.Test.3893811644._hygCtx._hyg.27 : ((And #4) #3)) => #3)) #1) #0)))))))
checked 4 declarations, 1 failed, in 0.00406485s wall (2.4525e-06 core-hours over 4 workers); 0 reduction steps; peak 21 MB in one worker

Test "corner-cases/eta-struct-major-and-no-whnf"

Expected: 🤷 either · Size: 24.0 KB · Lines: 421 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ⌛ timeout · exit code -9 · wall time: 1.0 m · max rss memory: 0 B

stderr:

Killed after exceeding the timeout of 1.0 m.
loaded 18 declarations, 309 exprs (309 unique), 89 names in 0.000368321s
declaration order verified in 3.095e-06s
environment built in 2.7361e-05s; checking with 4 worker processes

Test "corner-cases/eta-struct-major-no-whnf"

Expected: 🤷 either · Size: 32.2 KB · Lines: 582 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ⌛ timeout · exit code -9 · wall time: 1.0 m · max rss memory: 0 B

stderr:

Killed after exceeding the timeout of 1.0 m.
loaded 22 declarations, 434 exprs (434 unique), 118 names in 0.000386634s
declaration order verified in 6.802e-06s
environment built in 2.3714e-05s; checking with 4 worker processes

Test "corner-cases/eta-unit-like-nested"

Expected: 🤷 either · Size: 16.0 KB · Lines: 256 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 35 ms · instructions: 8.1 M · max rss memory: 21.6 MB

stderr:

loaded 9 declarations, 191 exprs (191 unique), 51 names in 0.000458589s
declaration order verified in 4.358e-06s
environment built in 5.0535e-05s; checking with 4 worker processes
FAIL unitLikeNested (line 256): declaration type mismatch for 'unitLikeNested'
  inferred: ((p : ((Mixed Nat) ((a._@._internal._hyg.0 : Bool) -> UnitField))) -> ((a : ((Mixed Nat) ((a._@._internal._hyg.0 : Bool) -> UnitField))) -> (((Eq.{1} ((Mixed Nat) ((a._@._internal._hyg.0 : Bool) -> UnitField))) #0) #0)))
  declared: ((p : ((Mixed Nat) ((a._@._internal._hyg.0 : Bool) -> UnitField))) -> ((q : ((Mixed Nat) ((a._@._internal._hyg.0 : Bool) -> UnitField))) -> (((Eq.{1} ((Mixed Nat) ((a._@._internal._hyg.0 : Bool) -> UnitField))) #1) #0)))
checked 8 declarations, 1 failed, in 0.00840248s wall (5.02684e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "corner-cases/eta-unit-like-pi"

Expected: 🤷 either · Size: 5.6 KB · Lines: 101 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 25 ms · instructions: 6.9 M · max rss memory: 21.6 MB

stderr:

loaded 4 declarations, 71 exprs (71 unique), 22 names in 0.000211025s
declaration order verified in 9.297e-06s
environment built in 2.3844e-05s; checking with 4 worker processes
FAIL unitLikePi (line 101): declaration type mismatch for 'unitLikePi'
  inferred: ((α : Sort(1)) -> ((p : ((a._@._internal._hyg.0 : #0) -> Unit)) -> ((q : ((a._@._internal._hyg.0 : #1) -> Unit)) -> (((Eq.{1} ((a._@._internal._hyg.0 : #2) -> Unit)) #0) #0))))
  declared: ((α : Sort(1)) -> ((p : ((a._@._internal._hyg.0 : #0) -> Unit)) -> ((q : ((a._@._internal._hyg.0 : #1) -> Unit)) -> (((Eq.{1} ((a._@._internal._hyg.0 : #2) -> Unit)) #1) #0))))
checked 3 declarations, 1 failed, in 0.00282311s wall (2.2922e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "corner-cases/eta-unit-like-proof-field"

Expected: 🤷 either · Size: 6.5 KB · Lines: 111 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 25 ms · instructions: 7.0 M · max rss memory: 21.6 MB

stderr:

loaded 4 declarations, 78 exprs (78 unique), 25 names in 0.000273983s
declaration order verified in 2.985e-06s
environment built in 2.3554e-05s; checking with 4 worker processes
FAIL unitLikeProofField (line 111): declaration type mismatch for 'unitLikeProofField'
  inferred: ((p : ProofField) -> ((a : ProofField) -> (((Eq.{1} ProofField) #0) #0)))
  declared: ((p : ProofField) -> ((q : ProofField) -> (((Eq.{1} ProofField) #1) #0)))
checked 3 declarations, 1 failed, in 0.00336634s wall (2.4918e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "corner-cases/eta-unit-like-struct"

Expected: 🤷 either · Size: 6.7 KB · Lines: 115 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 27 ms · instructions: 7.0 M · max rss memory: 21.7 MB

stderr:

loaded 5 declarations, 80 exprs (80 unique), 26 names in 0.000226184s
declaration order verified in 4.398e-06s
environment built in 3.0618e-05s; checking with 4 worker processes
FAIL unitLikeStruct (line 115): declaration type mismatch for 'unitLikeStruct'
  inferred: ((p : UnitField) -> ((a : UnitField) -> (((Eq.{1} UnitField) #0) #0)))
  declared: ((p : UnitField) -> ((q : UnitField) -> (((Eq.{1} UnitField) #1) #0)))
checked 4 declarations, 1 failed, in 0.00335386s wall (2.78332e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "corner-cases/imax-right-successor"

Expected: 🤷 either · Size: 806 B · Lines: 21 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 29 ms · instructions: 6.3 M · max rss memory: 21.6 MB

stderr:

loaded 2 declarations, 4 exprs (4 unique), 4 names in 0.000238687s
declaration order verified in 1.5138e-05s
environment built in 2.8895e-05s; checking with 4 worker processes
FAIL imaxRightOne (line 11): declaration type mismatch for 'imaxRightOne'
  inferred: Sort((imax u 1)+1)
  declared: Sort((max u 1)+1)
checked 0 declarations, 1 failed, in 0.00506972s wall (2.3091e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "corner-cases/let-value-type-mismatch"

Expected: 🤷 either · Size: 601 B · Lines: 13 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

def EcosystemCase : Sort 2 := let u : Sort 1 := Sort 1; u

Test result: ✋ rejected · exit code 1 · wall time: 32 ms · instructions: 6.3 M · max rss memory: 21.7 MB

stderr:

loaded 1 declarations, 5 exprs (5 unique), 4 names in 0.000241643s
declaration order verified in 3.757e-06s
environment built in 2.4646e-05s; checking with 4 worker processes
FAIL EcosystemCase (line 13): let value type mismatch for 'u'
checked 0 declarations, 1 failed, in 0.00668065s wall (3.74401e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "corner-cases/nested-nonuniform-param"

Expected: 🤷 either · Size: 9.2 KB · Lines: 142 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 29 ms · instructions: 7.6 M · max rss memory: 21.7 MB

stderr:

loaded 4 declarations, 108 exprs (108 unique), 27 names in 0.000405409s
declaration order verified in 7.825e-06s
environment built in 2.129e-05s; checking with 4 worker processes
checked 4 declarations, 0 failed, in 0.0040662s wall (2.97779e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "corner-cases/positivity-whnf"

Expected: 🤷 either · Size: 4.7 KB · Lines: 81 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

def Ignore (A B : Type) : Type := A

inductive T : Type where
  | mk (f : Ignore Unit T -> T) : T

Test result: ✋ rejected · exit code 1 · wall time: 37 ms · instructions: 6.6 M · max rss memory: 21.6 MB

stderr:

loaded 4 declarations, 50 exprs (50 unique), 23 names in 0.000827359s
declaration order verified in 2.3134e-05s
environment built in 2.9525e-05s; checking with 4 worker processes
FAIL LALReduciblePositivity (line 81): arg #1 of 'LALReduciblePositivity.mk' has a non positive occurrence of the datatypes being declared
checked 3 declarations, 1 failed, in 0.00711132s wall (5.66241e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "corner-cases/proj-maybe-prop"

Expected: 🤷 either · Size: 8.1 KB · Lines: 131 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 35 ms · instructions: 7.2 M · max rss memory: 21.8 MB

stderr:

loaded 5 declarations, 92 exprs (92 unique), 31 names in 0.00053905s
declaration order verified in 3.537e-06s
environment built in 2.8303e-05s; checking with 4 worker processes
checked 5 declarations, 0 failed, in 0.00389852s wall (3.26269e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "corner-cases/proj-maybe-prop-past"

Expected: 🤷 either · Size: 8.1 KB · Lines: 131 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 36 ms · instructions: 7.1 M · max rss memory: 21.7 MB

stderr:

loaded 5 declarations, 92 exprs (92 unique), 31 names in 0.000483255s
declaration order verified in 3.667e-06s
environment built in 3.3893e-05s; checking with 4 worker processes
checked 5 declarations, 0 failed, in 0.00783918s wall (5.63184e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "corner-cases/proof-param-ok"

Expected: 👍 accept · Size: 2.9 KB · Lines: 53 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Test result: 👍 accepted · exit code 0 · wall time: 32 ms · instructions: 6.6 M · max rss memory: 21.8 MB

stderr:

loaded 1 declarations, 39 exprs (39 unique), 10 names in 0.000439773s
declaration order verified in 6.221e-06s
environment built in 2.7411e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00636536s wall (3.76003e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "corner-cases/proof-param-swap"

Expected: 🤷 either · Size: 2.9 KB · Lines: 53 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Test result: ✋ rejected · exit code 1 · wall time: 33 ms · instructions: 6.5 M · max rss memory: 21.7 MB

stderr:

loaded 1 declarations, 39 exprs (39 unique), 10 names in 0.00043803s
declaration order verified in 9.338e-06s
environment built in 2.9105e-05s; checking with 4 worker processes
FAIL LALProofParameterSwap (line 53): invalid return type for 'LALProofParameterSwap.mk'
checked 0 declarations, 1 failed, in 0.00703697s wall (3.7105e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "corner-cases/subject-reduction-redex"

Expected: 🤷 either · Size: 66.6 KB · Lines: 1.2 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 41 ms · instructions: 17.9 M · max rss memory: 22.3 MB

stderr:

loaded 42 declarations, 924 exprs (924 unique), 206 names in 0.0007316s
declaration order verified in 1.3405e-05s
environment built in 4.9984e-05s; checking with 4 worker processes
checked 42 declarations, 0 failed, in 0.0136339s wall (1.20089e-05 core-hours over 4 workers); 681 reduction steps; peak 22 MB in one worker

Test "corner-cases/subject-reduction-reduct"

Expected: 🤷 either · Size: 65.5 KB · Lines: 1.2 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 38 ms · instructions: 17.4 M · max rss memory: 22.9 MB

stderr:

loaded 41 declarations, 906 exprs (906 unique), 202 names in 0.000876341s
declaration order verified in 1.9627e-05s
environment built in 6.0864e-05s; checking with 4 worker processes
FAIL reduct (line 1165): application type mismatch in ($11 $12)
  argument type: ($9 ((f (((OfNat.ofNat.{0} Nat) 1) (instOfNatNat 1))) $8))
  expected: ($9 ((f (((OfNat.ofNat.{0} Nat) 0) (instOfNatNat 0))) (redex._proof_1 $8)))
checked 40 declarations, 1 failed, in 0.0121868s wall (1.09383e-05 core-hours over 4 workers); 522 reduction steps; peak 22 MB in one worker

Test "cslib"

Expected: 👍 accept · Size: 2.3 GB · Lines: 42.7 M · lean4export: 3.1.0 · Lean: 4.34.0 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 2.1 m · instructions: 1.7 T · max rss memory: 2.5 GB

stderr:

loaded 383976 declarations, 40045123 exprs (40045123 unique), 2248524 names in 12.7817s
declaration order verified in 0.500623s
environment built in 0.253995s; checking with 4 worker processes
checked 383976 declarations, 0 failed, in 112.383s wall (0.124815 core-hours over 4 workers); 226710711 reduction steps; peak 2570 MB in one worker

Test "init"

Expected: 👍 accept · Size: 331.5 MB · Lines: 6.5 M · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 10.5 s · instructions: 221.8 G · max rss memory: 392.0 MB

stderr:

loaded 58170 declarations, 6132277 exprs (6132277 unique), 296040 names in 0.770717s
declaration order verified in 0.0419569s
environment built in 0.0216061s; checking with 4 worker processes
checked 58170 declarations, 0 failed, in 9.64731s wall (0.010701 core-hours over 4 workers); 51915309 reduction steps; peak 391 MB in one worker

Test "init-prelude"

Expected: 👍 accept · Size: 3.6 MB · Lines: 64.1 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 57 ms · instructions: 607.6 M · max rss memory: 29.4 MB

stderr:

loaded 1824 declarations, 54799 exprs (54799 unique), 7373 names in 0.00898535s
declaration order verified in 0.000339586s
environment built in 0.000490648s; checking with 4 worker processes
checked 1824 declarations, 0 failed, in 0.033876s wall (3.55742e-05 core-hours over 4 workers); 33480 reduction steps; peak 26 MB in one worker

Test "mathlib"

Expected: 👍 accept · Size: 5.8 GB · Lines: 109.8 M · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 9.1 m · instructions: 5.9 T · max rss memory: 7.0 GB

stderr:

loaded 702040 declarations, 104860875 exprs (104860875 unique), 4184135 names in 19.6254s
declaration order verified in 1.07783s
environment built in 0.500876s; checking with 4 worker processes
checked 702040 declarations, 0 failed, in 522.685s wall (0.580479 core-hours over 4 workers); 740844580 reduction steps; peak 7172 MB in one worker

Test "navier-stokes-euler"

Expected: 👍 accept · Size: 1.5 GB · Lines: 28.6 M · lean4export: 3.1.0 · Lean: 4.34.0-rc2 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 4.5 m · instructions: 2.4 T · max rss memory: 1.8 GB

stderr:

loaded 126468 declarations, 27747197 exprs (27747197 unique), 691465 names in 4.06756s
declaration order verified in 0.351429s
environment built in 0.0990128s; checking with 4 worker processes
checked 126468 declarations, 0 failed, in 268.638s wall (0.298468 core-hours over 4 workers); 405506772 reduction steps; peak 1778 MB in one worker

Test "other/extra-rec"

Expected: ✋ reject · Size: 1.4 KB · Lines: 21 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Test result: ✋ rejected · exit code 1 · wall time: 15 ms · instructions: 6.4 M · max rss memory: 21.8 MB

stderr:

loaded 2 declarations, 10 exprs (10 unique), 7 names in 0.000113002s
declaration order verified in 2.164e-06s
environment built in 1.5539e-05s; checking with 4 worker processes
FAIL False (line 18): recursor count mismatch for 'False': export has 2, derived 1
checked 0 declarations, 1 failed, in 0.00175226s wall (1.10752e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "other/level-index-out-of-order"

Expected: 👍 accept · Size: 328 B · Lines: 6 · lean4export: 0.1.0 · Lean: 4.29.1 · 📄 Declaration

Test result: 👍 accepted · exit code 0 · wall time: 19 ms · instructions: 6.2 M · max rss memory: 21.6 MB

stderr:

loaded 1 declarations, 1 exprs (1 unique), 1 names in 0.000147307s
declaration order verified in 2.255e-06s
environment built in 2.3855e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.0031088s wall (1.43195e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "other/nat-lit-add"

Expected: 👍 accept · Size: 26.0 KB · Lines: 478 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 19 ms · instructions: 9.4 M · max rss memory: 21.9 MB

stderr:

loaded 16 declarations, 363 exprs (363 unique), 90 names in 0.000829104s
declaration order verified in 4.989e-06s
environment built in 2.0268e-05s; checking with 4 worker processes
checked 16 declarations, 0 failed, in 0.00406637s wall (3.2585e-06 core-hours over 4 workers); 106 reduction steps; peak 20 MB in one worker

Test "other/nat-lit-add-bad"

Expected: ✋ reject · Size: 25.3 KB · Lines: 465 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

natAddLitBad : Nat.add 123456789 987654321 = 1111111111
  := Eq.refl (Nat.add 123456789 987654321)

Test result: ✋ rejected · exit code 1 · wall time: 21 ms · instructions: 9.4 M · max rss memory: 21.8 MB

stderr:

loaded 15 declarations, 352 exprs (352 unique), 89 names in 0.000926597s
declaration order verified in 5.56e-06s
environment built in 2.4736e-05s; checking with 4 worker processes
FAIL natAddLitBad (line 465): declaration type mismatch for 'natAddLitBad'
  inferred: (((Eq.{1} Nat) ((Nat.add (((OfNat.ofNat.{0} Nat) 123456789) (instOfNatNat 123456789))) (((OfNat.ofNat.{0} Nat) 987654321) (instOfNatNat 987654321)))) ((Nat.add (((OfNat.ofNat.{0} Nat) 123456789) (instOfNatNat 123456789))) (((OfNat.ofNat.{0} Nat) 987654321) (instOfNatNat 987654321))))
  declared: (((Eq.{1} Nat) ((Nat.add (((OfNat.ofNat.{0} Nat) 123456789) (instOfNatNat 123456789))) (((OfNat.ofNat.{0} Nat) 987654321) (instOfNatNat 987654321)))) (((OfNat.ofNat.{0} Nat) 1111111111) (instOfNatNat 1111111111)))
checked 14 declarations, 1 failed, in 0.00499733s wall (3.82407e-06 core-hours over 4 workers); 62 reduction steps; peak 21 MB in one worker

Test "other/nat-lit-ble"

Expected: 👍 accept · Size: 28.8 KB · Lines: 520 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 27 ms · instructions: 9.7 M · max rss memory: 21.8 MB

stderr:

loaded 17 declarations, 394 exprs (394 unique), 100 names in 0.000930153s
declaration order verified in 5.239e-06s
environment built in 3.4195e-05s; checking with 4 worker processes
checked 17 declarations, 0 failed, in 0.006456s wall (4.79418e-06 core-hours over 4 workers); 105 reduction steps; peak 20 MB in one worker

Test "other/nat-lit-sub"

Expected: 👍 accept · Size: 30.0 KB · Lines: 561 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 23 ms · instructions: 9.8 M · max rss memory: 21.9 MB

stderr:

loaded 20 declarations, 393 exprs (393 unique), 139 names in 0.000510627s
declaration order verified in 5.44e-06s
environment built in 2.8503e-05s; checking with 4 worker processes
checked 20 declarations, 0 failed, in 0.0048857s wall (4.07014e-06 core-hours over 4 workers); 129 reduction steps; peak 20 MB in one worker

Test "other/orphan-ctor"

Expected: ✋ reject · Size: 1.4 KB · Lines: 22 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Test result: ✋ rejected · exit code 1 · wall time: 19 ms · instructions: 6.4 M · max rss memory: 21.6 MB

stderr:

loaded 2 declarations, 10 exprs (10 unique), 8 names in 0.000137748s
declaration order verified in 2.394e-06s
environment built in 1.585e-05s; checking with 4 worker processes
FAIL False (line 19): constructor count mismatch in inductive block
checked 0 declarations, 1 failed, in 0.00317499s wall (1.38968e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "other/proj-of-prop"

Expected: ✋ reject · Size: 3.9 KB · Lines: 56 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

badFalse : False := (Wrapper.mk True.intro).p

Test result: ✋ rejected · exit code 1 · wall time: 18 ms · instructions: 6.7 M · max rss memory: 21.6 MB

stderr:

loaded 4 declarations, 35 exprs (35 unique), 15 names in 0.000649367s
declaration order verified in 4.648e-06s
environment built in 2.685e-05s; checking with 4 worker processes
FAIL badFalse (line 56): application type mismatch in (Wrapper.mk True.intro)
  argument type: True
  expected: False
checked 3 declarations, 1 failed, in 0.00286963s wall (1.73039e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "other/sparse-name-index"

Expected: 👍 accept · Size: 292 B · Lines: 4 · lean4export: 0.1.0 · Lean: 4.29.1 · 📄 Declaration

Test result: 👍 accepted · exit code 0 · wall time: 18 ms · instructions: 6.2 M · max rss memory: 21.7 MB

stderr:

loaded 1 declarations, 1 exprs (1 unique), 1 names in 0.000148859s
declaration order verified in 2.815e-06s
environment built in 1.8275e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.004248s wall (2.05399e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "perf/app-lam"

Expected: 👍 accept · Size: 1.2 MB · Lines: 28.6 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 2.5 s · instructions: 14.2 G · max rss memory: 78.0 MB

stderr:

loaded 22 declarations, 24430 exprs (24430 unique), 4110 names in 0.00519336s
declaration order verified in 4.6417e-05s
environment built in 2.3775e-05s; checking with 4 worker processes
checked 22 declarations, 0 failed, in 2.45043s wall (0.000681506 core-hours over 4 workers); 72 reduction steps; peak 77 MB in one worker

Test "perf/args-before-unfold"

Expected: 👍 accept · Size: 44.5 KB · Lines: 1.2 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

count #n      and      count (N.add #(n-1) #1)

Test result: 👍 accepted · exit code 0 · wall time: 28 ms · instructions: 32.9 M · max rss memory: 24.8 MB

stderr:

loaded 5 declarations, 1106 exprs (1106 unique), 43 names in 0.000749114s
declaration order verified in 6.222e-06s
environment built in 1.6181e-05s; checking with 4 worker processes
checked 5 declarations, 0 failed, in 0.0122932s wall (4.32649e-06 core-hours over 4 workers); 3006 reduction steps; peak 24 MB in one worker

Test "perf/beta-ladder"

Expected: 👍 accept · Size: 450.6 KB · Lines: 10.4 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

(fun x₁ => … (fun xₙ => x₁ + (x₂ + (… + (xₙ + 0)))) 0 …) 0

Test result: 👍 accepted · exit code 0 · wall time: 671 ms · instructions: 4.0 G · max rss memory: 47.4 MB

stderr:

loaded 12 declarations, 10284 exprs (10284 unique), 78 names in 0.00258107s
declaration order verified in 2.106e-05s
environment built in 2.4155e-05s; checking with 4 worker processes
checked 12 declarations, 0 failed, in 0.653189s wall (0.000183558 core-hours over 4 workers); 16057 reduction steps; peak 47 MB in one worker

Test "perf/church-numerals"

Expected: 👍 accept · Size: 9.6 KB · Lines: 227 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

cmul (cnum n) (cnum (n+1))      and      cmul (cnum (n+1)) (cnum n)

Test result: 👍 accepted · exit code 0 · wall time: 38 ms · instructions: 101.8 M · max rss memory: 31.5 MB

stderr:

loaded 4 declarations, 197 exprs (197 unique), 21 names in 0.000463379s
declaration order verified in 6.302e-06s
environment built in 1.8444e-05s; checking with 4 worker processes
checked 4 declarations, 0 failed, in 0.0227261s wall (7.18876e-06 core-hours over 4 workers); 253 reduction steps; peak 31 MB in one worker

Test "perf/discarded-argument"

Expected: 👍 accept · Size: 15.9 KB · Lines: 367 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

dropArg (count #n)      and      dropArg (count #(n+1))

Test result: 👍 accepted · exit code 0 · wall time: 31 ms · instructions: 59.3 M · max rss memory: 25.0 MB

stderr:

loaded 6 declarations, 309 exprs (309 unique), 48 names in 0.000665838s
declaration order verified in 8.286e-06s
environment built in 2.5879e-05s; checking with 4 worker processes
checked 6 declarations, 0 failed, in 0.0139732s wall (5.18802e-06 core-hours over 4 workers); 14803 reduction steps; peak 24 MB in one worker

Test "perf/discarded-argument-match"

Expected: 👍 accept · Size: 29.2 KB · Lines: 606 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

dropArg (count #n)      and      dropArg (count #(n+1))

Test result: 👍 accepted · exit code 0 · wall time: 50 ms · instructions: 216.5 M · max rss memory: 25.3 MB

stderr:

loaded 17 declarations, 496 exprs (496 unique), 85 names in 0.00052822s
declaration order verified in 5.25e-06s
environment built in 2.0789e-05s; checking with 4 worker processes
checked 17 declarations, 0 failed, in 0.0326205s wall (1.15305e-05 core-hours over 4 workers); 46358 reduction steps; peak 25 MB in one worker

Test "perf/folded-constant-first"

Expected: 👍 accept · Size: 52.0 KB · Lines: 1.3 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

tagged (count #n)      and      (false, count #n)

Test result: 👍 accepted · exit code 0 · wall time: 27 ms · instructions: 29.0 M · max rss memory: 26.8 MB

stderr:

loaded 9 declarations, 1180 exprs (1180 unique), 65 names in 0.000552005s
declaration order verified in 5.851e-06s
environment built in 1.9457e-05s; checking with 4 worker processes
checked 9 declarations, 0 failed, in 0.0110127s wall (4.45868e-06 core-hours over 4 workers); 20033 reduction steps; peak 26 MB in one worker

Test "perf/folded-constant-last"

Expected: 👍 accept · Size: 51.0 KB · Lines: 1.3 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

tagged (count #n)      and      (count #n, false)

Test result: 👍 accepted · exit code 0 · wall time: 28 ms · instructions: 29.0 M · max rss memory: 26.8 MB

stderr:

loaded 9 declarations, 1180 exprs (1180 unique), 65 names in 0.00114226s
declaration order verified in 7.444e-06s
environment built in 2.663e-05s; checking with 4 worker processes
checked 9 declarations, 0 failed, in 0.00999062s wall (4.49205e-06 core-hours over 4 workers); 20033 reduction steps; peak 26 MB in one worker

Test "perf/fueled-chain"

Expected: 👍 accept · Size: 848.6 KB · Lines: 17.3 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 97 ms · instructions: 614.2 M · max rss memory: 26.9 MB

stderr:

loaded 143 declarations, 16168 exprs (16168 unique), 942 names in 0.0043628s
declaration order verified in 7.0753e-05s
environment built in 7.6564e-05s; checking with 4 worker processes
checked 143 declarations, 0 failed, in 0.0736392s wall (4.26464e-05 core-hours over 4 workers); 13621 reduction steps; peak 26 MB in one worker

Test "perf/grind-ring-5"

Expected: 👍 accept · Size: 9.8 MB · Lines: 200.3 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 560 ms · instructions: 4.9 G · max rss memory: 86.3 MB

stderr:

loaded 2273 declarations, 181939 exprs (181939 unique), 16048 names in 0.0325353s
declaration order verified in 0.000897783s
environment built in 0.000503915s; checking with 4 worker processes
checked 2273 declarations, 0 failed, in 0.510402s wall (0.000294453 core-hours over 4 workers); 2375752 reduction steps; peak 86 MB in one worker

Test "perf/identical-nesting"

Expected: 👍 accept · Size: 8.7 KB · Lines: 172 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

f4 (f4 (... (f4 N.O) ...))      and      f4 (f4 (... (f4 N.O) ...))

Test result: 👍 accepted · exit code 0 · wall time: 17 ms · instructions: 7.1 M · max rss memory: 21.5 MB

stderr:

loaded 8 declarations, 128 exprs (128 unique), 32 names in 0.000699712s
declaration order verified in 4.9e-06s
environment built in 1.8485e-05s; checking with 4 worker processes
checked 8 declarations, 0 failed, in 0.00274816s wall (2.06691e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "perf/irrelevance-before-evaluation"

Expected: 👍 accept · Size: 17.5 KB · Lines: 388 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

slowTriv (count #n) = True.intro

Test result: 👍 accepted · exit code 0 · wall time: 22 ms · instructions: 7.5 M · max rss memory: 21.6 MB

stderr:

loaded 7 declarations, 324 exprs (324 unique), 53 names in 0.000587902s
declaration order verified in 5.461e-06s
environment built in 1.3826e-05s; checking with 4 worker processes
checked 7 declarations, 0 failed, in 0.00295081s wall (1.88514e-06 core-hours over 4 workers); 9 reduction steps; peak 19 MB in one worker

Test "perf/let-fold"

Expected: 👍 accept · Size: 316.9 KB · Lines: 6.0 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

let d := bits #n 0; (rfl : d + 0 = Nat.add d 0)

Test result: 👍 accepted · exit code 0 · wall time: 29 ms · instructions: 69.8 M · max rss memory: 22.9 MB

stderr:

loaded 156 declarations, 4800 exprs (4800 unique), 1017 names in 0.0012998s
declaration order verified in 1.7914e-05s
environment built in 5.4543e-05s; checking with 4 worker processes
checked 156 declarations, 0 failed, in 0.0118579s wall (1.09675e-05 core-hours over 4 workers); 3520 reduction steps; peak 22 MB in one worker

Test "perf/let-ladder"

Expected: 👍 accept · Size: 457.6 KB · Lines: 10.4 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

let x₃ := 0; x₃ + (let x₂ := 0; x₂ + (let x₁ := 0; x₁ + (x₃ + (x₂ + (x₁ + 0)))))

Test result: 👍 accepted · exit code 0 · wall time: 578 ms · instructions: 2.2 G · max rss memory: 36.9 MB

stderr:

loaded 14 declarations, 10295 exprs (10295 unique), 85 names in 0.00238785s
declaration order verified in 2.7301e-05s
environment built in 2.8784e-05s; checking with 4 worker processes
checked 14 declarations, 0 failed, in 0.560602s wall (0.000158141 core-hours over 4 workers); 2062 reduction steps; peak 36 MB in one worker

Test "perf/magma-list-deep-n21"

Expected: 👍 accept · Size: 1.1 MB · Lines: 21.8 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 223 ms · instructions: 2.3 G · max rss memory: 29.8 MB

stderr:

loaded 514 declarations, 17865 exprs (17865 unique), 3436 names in 0.00525939s
declaration order verified in 6.8288e-05s
environment built in 0.000153317s; checking with 4 worker processes
checked 514 declarations, 0 failed, in 0.200705s wall (6.87878e-05 core-hours over 4 workers); 2803318 reduction steps; peak 29 MB in one worker

Test "perf/magma-list-deep-n36"

Expected: 👍 accept · Size: 1.2 MB · Lines: 23.0 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 3.1 s · instructions: 31.3 G · max rss memory: 47.1 MB

stderr:

loaded 514 declarations, 18986 exprs (18986 unique), 3508 names in 0.00585602s
declaration order verified in 0.000102622s
environment built in 0.000192811s; checking with 4 worker processes
checked 514 declarations, 0 failed, in 3.05743s wall (0.00086873 core-hours over 4 workers); 47638593 reduction steps; peak 47 MB in one worker

Test "perf/magma-list-pair-n21"

Expected: 👍 accept · Size: 583.1 KB · Lines: 11.0 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 10.7 s · instructions: 38.0 G · max rss memory: 1.3 GB

stderr:

loaded 276 declarations, 8828 exprs (8828 unique), 1898 names in 0.00521258s
declaration order verified in 2.7852e-05s
environment built in 0.000121588s; checking with 4 worker processes
checked 276 declarations, 0 failed, in 10.724s wall (0.00295447 core-hours over 4 workers); 33690557 reduction steps; peak 1365 MB in one worker

Test "perf/magma-list-pair-n7"

Expected: 👍 accept · Size: 583.6 KB · Lines: 11.0 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 713 ms · instructions: 3.2 G · max rss memory: 128.7 MB

stderr:

loaded 276 declarations, 8838 exprs (8838 unique), 1898 names in 0.00280436s
declaration order verified in 2.9165e-05s
environment built in 0.000164699s; checking with 4 worker processes
checked 276 declarations, 0 failed, in 0.694817s wall (0.000201894 core-hours over 4 workers); 2519725 reduction steps; peak 128 MB in one worker

Test "perf/magma-string-n4"

Expected: 👍 accept · Size: 16.5 MB · Lines: 344.3 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 570 ms · instructions: 11.0 G · max rss memory: 55.5 MB

stderr:

loaded 3268 declarations, 321312 exprs (321312 unique), 19661 names in 0.0536462s
declaration order verified in 0.00142644s
environment built in 0.000577302s; checking with 4 worker processes
checked 3268 declarations, 0 failed, in 0.500533s wall (0.000532725 core-hours over 4 workers); 3310447 reduction steps; peak 52 MB in one worker

Test "perf/magma-string-pair-n9"

Expected: 👍 accept · Size: 16.6 MB · Lines: 344.3 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 1.9 s · instructions: 20.6 G · max rss memory: 158.4 MB

stderr:

loaded 3268 declarations, 321333 exprs (321333 unique), 19661 names in 0.0468196s
declaration order verified in 0.00138017s
environment built in 0.000562655s; checking with 4 worker processes
checked 3268 declarations, 0 failed, in 1.802s wall (0.000849607 core-hours over 4 workers); 14189521 reduction steps; peak 158 MB in one worker

Test "perf/proj-cheap-struct"

Expected: 👍 accept · Size: 85.9 KB · Lines: 1.5 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

(S u).re      and      (S ()).re

Test result: 👍 accepted · exit code 0 · wall time: 18 ms · instructions: 16.9 M · max rss memory: 22.0 MB

stderr:

loaded 57 declarations, 1164 exprs (1164 unique), 300 names in 0.000721402s
declaration order verified in 6.603e-06s
environment built in 2.5768e-05s; checking with 4 worker processes
checked 57 declarations, 0 failed, in 0.00571922s wall (5.23677e-06 core-hours over 4 workers); 257 reduction steps; peak 21 MB in one worker

Test "perf/proj-lazy-struct"

Expected: 👍 accept · Size: 44.9 KB · Lines: 808 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

(P (slow 100000)).1      and      (Q (slow 100001)).1

Test result: 👍 accepted · exit code 0 · wall time: 16 ms · instructions: 11.7 M · max rss memory: 22.0 MB

stderr:

loaded 31 declarations, 613 exprs (613 unique), 148 names in 0.000722935s
declaration order verified in 3.537e-06s
environment built in 2.3144e-05s; checking with 4 worker processes
checked 31 declarations, 0 failed, in 0.00358944s wall (3.2083e-06 core-hours over 4 workers); 120 reduction steps; peak 21 MB in one worker

Test "perf/proj-stuck-struct"

Expected: 👍 accept · Size: 50.1 KB · Lines: 916 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 18 ms · instructions: 12.4 M · max rss memory: 21.9 MB

stderr:

loaded 34 declarations, 711 exprs (711 unique), 155 names in 0.000683331s
declaration order verified in 7.544e-06s
environment built in 3.0106e-05s; checking with 4 worker processes
checked 34 declarations, 0 failed, in 0.00444393s wall (3.91179e-06 core-hours over 4 workers); 139 reduction steps; peak 21 MB in one worker

Test "perf/refute-cheap-first"

Expected: ✋ reject · Size: 20.7 KB · Lines: 439 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

(false, count #n) = (true, count #(n+1))

Test result: ✋ rejected · exit code 1 · wall time: 26 ms · instructions: 60.8 M · max rss memory: 25.6 MB

stderr:

loaded 7 declarations, 367 exprs (367 unique), 57 names in 0.000284904s
declaration order verified in 2.705e-06s
environment built in 1.4958e-05s; checking with 4 worker processes
FAIL kernel_refute_cheap_first (line 439): declaration type mismatch for 'kernel_refute_cheap_first'
  inferred: (((Eq.{1} ((Prod.{0, 0} Bool) N)) ((((Prod.mk.{0, 0} Bool) N) Bool.false) (count (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S N.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ((((Prod.mk.{0, 0} Bool) N) Bool.false) (count (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S N.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  declared: (((Eq.{1} ((Prod.{0, 0} Bool) N)) ((((Prod.mk.{0, 0} Bool) N) Bool.false) (count (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S N.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ((((Prod.mk.{0, 0} Bool) N) Bool.true) (count (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S N.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
checked 6 declarations, 1 failed, in 0.0129026s wall (4.78401e-06 core-hours over 4 workers); 6 reduction steps; peak 25 MB in one worker

Test "perf/refute-cheap-last"

Expected: ✋ reject · Size: 20.5 KB · Lines: 439 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

(count #n, false) = (count #(n+1), true)

Test result: ✋ rejected · exit code 1 · wall time: 26 ms · instructions: 61.1 M · max rss memory: 25.8 MB

stderr:

loaded 7 declarations, 367 exprs (367 unique), 57 names in 0.000302998s
declaration order verified in 2.425e-06s
environment built in 2.134e-05s; checking with 4 worker processes
FAIL kernel_refute_cheap_last (line 439): declaration type mismatch for 'kernel_refute_cheap_last'
  inferred: (((Eq.{1} ((Prod.{0, 0} N) Bool)) ((((Prod.mk.{0, 0} N) Bool) (count (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S N.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) Bool.false)) ((((Prod.mk.{0, 0} N) Bool) (count (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S N.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) Bool.false))
  declared: (((Eq.{1} ((Prod.{0, 0} N) Bool)) ((((Prod.mk.{0, 0} N) Bool) (count (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S N.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) Bool.false)) ((((Prod.mk.{0, 0} N) Bool) (count (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S (N.S N.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) Bool.true))
checked 6 declarations, 1 failed, in 0.0119428s wall (4.3189e-06 core-hours over 4 workers); 6 reduction steps; peak 25 MB in one worker

Test "perf/repeated-subproblem"

Expected: 👍 accept · Size: 11.4 KB · Lines: 214 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

perfect #n leaf      and      perfect #(n-1) (node leaf leaf)

Test result: 👍 accepted · exit code 0 · wall time: 17 ms · instructions: 8.2 M · max rss memory: 21.5 MB

stderr:

loaded 5 declarations, 162 exprs (162 unique), 43 names in 0.000385953s
declaration order verified in 2.405e-06s
environment built in 1.4106e-05s; checking with 4 worker processes
checked 5 declarations, 0 failed, in 0.00375416s wall (2.12323e-06 core-hours over 4 workers); 132 reduction steps; peak 20 MB in one worker

Test "perf/shared-subterm"

Expected: 👍 accept · Size: 50.1 KB · Lines: 1.3 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

ldepth (perfect #n leaf)      and      ldepth2 (perfect #n leaf)

Test result: 👍 accepted · exit code 0 · wall time: 32 ms · instructions: 111.4 M · max rss memory: 28.7 MB

stderr:

loaded 8 declarations, 1175 exprs (1175 unique), 65 names in 0.000376275s
declaration order verified in 5.34e-06s
environment built in 1.3896e-05s; checking with 4 worker processes
checked 8 declarations, 0 failed, in 0.0198497s wall (6.28224e-06 core-hours over 4 workers); 50009 reduction steps; peak 28 MB in one worker

Test "perf/shift-cascade"

Expected: 👍 accept · Size: 256.3 KB · Lines: 5.1 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 65 ms · instructions: 528.5 M · max rss memory: 33.3 MB

stderr:

loaded 5 declarations, 4089 exprs (4089 unique), 1032 names in 0.0012834s
declaration order verified in 1.1471e-05s
environment built in 2.0729e-05s; checking with 4 worker processes
checked 5 declarations, 0 failed, in 0.0512253s wall (1.48786e-05 core-hours over 4 workers); 1000 reduction steps; peak 33 MB in one worker

Test "perf/unroll-versus-evaluate"

Expected: 👍 accept · Size: 44.6 KB · Lines: 1.2 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

count #(n+1)      and      N.add (count #n) #1

Test result: 👍 accepted · exit code 0 · wall time: 16 ms · instructions: 8.3 M · max rss memory: 21.8 MB

stderr:

loaded 5 declarations, 1107 exprs (1107 unique), 43 names in 0.000438622s
declaration order verified in 3.427e-06s
environment built in 1.4347e-05s; checking with 4 worker processes
checked 5 declarations, 0 failed, in 0.00279069s wall (2.13275e-06 core-hours over 4 workers); 17 reduction steps; peak 19 MB in one worker

Test "std"

Expected: 👍 accept · Size: 569.0 MB · Lines: 10.8 M · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 21.2 s · instructions: 369.8 G · max rss memory: 710.3 MB

stderr:

loaded 101286 declarations, 10145829 exprs (10145829 unique), 578589 names in 1.65928s
declaration order verified in 0.0952641s
environment built in 0.0411138s; checking with 4 worker processes
checked 101286 declarations, 0 failed, in 19.5066s wall (0.0216592 core-hours over 4 workers); 77160347 reduction steps; peak 710 MB in one worker

Test "tutorial/001_basicDef"

Expected: 👍 accept · Size: 367 B · Lines: 6 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 15 ms · instructions: 6.3 M · max rss memory: 21.6 MB

stderr:

loaded 1 declarations, 2 exprs (2 unique), 1 names in 8.7454e-05s
declaration order verified in 1.753e-06s
environment built in 1.4828e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00235438s wall (1.33168e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/002_badDef"

Expected: ✋ reject · Size: 365 B · Lines: 6 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 20 ms · instructions: 6.3 M · max rss memory: 21.7 MB

stderr:

loaded 1 declarations, 2 exprs (2 unique), 1 names in 0.000142788s
declaration order verified in 2.214e-06s
environment built in 2.2873e-05s; checking with 4 worker processes
FAIL badDef (line 6): declaration type mismatch for 'badDef'
  inferred: Sort(2)
  declared: Sort(0)
checked 0 declarations, 1 failed, in 0.00250143s wall (1.45049e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/003_arrowType"

Expected: 👍 accept · Size: 622 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 19 ms · instructions: 6.3 M · max rss memory: 21.5 MB

stderr:

loaded 1 declarations, 3 exprs (3 unique), 6 names in 0.000218049s
declaration order verified in 2.334e-06s
environment built in 2.0779e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00328258s wall (2.02338e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/004_dependentType"

Expected: 👍 accept · Size: 460 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 18 ms · instructions: 6.3 M · max rss memory: 21.6 MB

stderr:

loaded 1 declarations, 3 exprs (3 unique), 2 names in 0.000117902s
declaration order verified in 1.844e-06s
environment built in 2.2813e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00311821s wall (1.75257e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/005_constType"

Expected: 👍 accept · Size: 897 B · Lines: 17 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 20 ms · instructions: 6.3 M · max rss memory: 21.6 MB

stderr:

loaded 1 declarations, 6 exprs (6 unique), 8 names in 0.000164639s
declaration order verified in 5.07e-06s
environment built in 2.3324e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00238604s wall (1.7429e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/006_betaReduction"

Expected: 👍 accept · Size: 1.3 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 17 ms · instructions: 6.3 M · max rss memory: 21.7 MB

stderr:

loaded 2 declarations, 13 exprs (13 unique), 10 names in 0.000167564s
declaration order verified in 2.083e-06s
environment built in 1.9296e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00237648s wall (1.25331e-06 core-hours over 4 workers); 1 reduction steps; peak 18 MB in one worker

Test "tutorial/007_betaReduction2"

Expected: 👍 accept · Size: 1.4 KB · Lines: 28 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 19 ms · instructions: 6.3 M · max rss memory: 21.4 MB

stderr:

loaded 2 declarations, 14 exprs (14 unique), 10 names in 9.4898e-05s
declaration order verified in 2.224e-06s
environment built in 1.1141e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00308669s wall (2.00031e-06 core-hours over 4 workers); 1 reduction steps; peak 18 MB in one worker

Test "tutorial/008_forallSortWhnf"

Expected: 👍 accept · Size: 1.2 KB · Lines: 25 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 18 ms · instructions: 6.3 M · max rss memory: 21.7 MB

stderr:

loaded 2 declarations, 13 exprs (13 unique), 6 names in 0.000145743s
declaration order verified in 2.294e-06s
environment built in 2.5658e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00263095s wall (1.9565e-06 core-hours over 4 workers); 8 reduction steps; peak 18 MB in one worker

Test "tutorial/009_forallSortBad"

Expected: ✋ reject · Size: 1.2 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 17 ms · instructions: 6.4 M · max rss memory: 21.7 MB

stderr:

loaded 2 declarations, 14 exprs (14 unique), 6 names in 0.000199383s
declaration order verified in 1.783e-06s
environment built in 1.2463e-05s; checking with 4 worker processes
FAIL forallSortBad (line 26): type expected: $1
checked 1 declarations, 1 failed, in 0.00166704s wall (1.22846e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/010_nonTypeType"

Expected: ✋ reject · Size: 1.1 KB · Lines: 21 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 14 ms · instructions: 6.3 M · max rss memory: 21.5 MB

stderr:

loaded 2 declarations, 8 exprs (8 unique), 9 names in 0.00014385s
declaration order verified in 5.691e-06s
environment built in 1.4076e-05s; checking with 4 worker processes
FAIL nonTypeType (line 21): type expected: constType
checked 1 declarations, 1 failed, in 0.0017984s wall (1.3576e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/011_nonTypeAxiom"

Expected: ✋ reject · Size: 1.0 KB · Lines: 20 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 17 ms · instructions: 6.3 M · max rss memory: 21.7 MB

stderr:

loaded 2 declarations, 7 exprs (7 unique), 9 names in 0.000125475s
declaration order verified in 1.904e-06s
environment built in 1.4898e-05s; checking with 4 worker processes
FAIL nonTypeAxiom (line 20): type expected: constType
checked 1 declarations, 1 failed, in 0.00176548s wall (1.11011e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/012_nonPropThm"

Expected: ✋ reject · Size: 424 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 17 ms · instructions: 6.3 M · max rss memory: 21.6 MB

stderr:

loaded 1 declarations, 3 exprs (3 unique), 2 names in 0.00014903s
declaration order verified in 1.783e-06s
environment built in 1.1622e-05s; checking with 4 worker processes
FAIL nonPropThm (line 7): theorem type is not a proposition: nonPropThm
checked 0 declarations, 1 failed, in 0.00224273s wall (1.52884e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/013_thmProof"

Expected: 👍 accept · Size: 1.3 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 15 ms · instructions: 6.3 M · max rss memory: 21.8 MB

stderr:

loaded 2 declarations, 14 exprs (14 unique), 9 names in 0.000154941s
declaration order verified in 2.615e-06s
environment built in 1.5198e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00207566s wall (1.27605e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/014_selfProof"

Expected: ✋ reject · Size: 459 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 15 ms · instructions: 6.3 M · max rss memory: 21.6 MB

stderr:

loaded 1 declarations, 4 exprs (4 unique), 2 names in 0.000150793s
declaration order verified in 2.024e-06s
environment built in 1.1542e-05s; checking with 4 worker processes
FAIL selfProof (line 8): unknown constant 'selfProof'
checked 0 declarations, 1 failed, in 0.00222049s wall (1.44342e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/015_levelComp1"

Expected: 👍 accept · Size: 391 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 16 ms · instructions: 6.3 M · max rss memory: 21.7 MB

stderr:

loaded 1 declarations, 2 exprs (2 unique), 1 names in 0.000128711s
declaration order verified in 1.813e-06s
environment built in 1.2564e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00185511s wall (1.17362e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/016_levelComp2"

Expected: 👍 accept · Size: 409 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 16 ms · instructions: 6.3 M · max rss memory: 21.5 MB

stderr:

loaded 1 declarations, 2 exprs (2 unique), 1 names in 0.000158878s
declaration order verified in 4.929e-06s
environment built in 1.3606e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00189173s wall (1.37567e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/017_levelComp3"

Expected: 👍 accept · Size: 427 B · Lines: 9 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 14 ms · instructions: 6.3 M · max rss memory: 21.7 MB

stderr:

loaded 1 declarations, 2 exprs (2 unique), 1 names in 0.000101821s
declaration order verified in 1.954e-06s
environment built in 1.6261e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00179487s wall (1.02825e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/018_levelParams"

Expected: 👍 accept · Size: 1.4 KB · Lines: 29 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 17 ms · instructions: 6.3 M · max rss memory: 21.7 MB

stderr:

loaded 2 declarations, 13 exprs (13 unique), 11 names in 0.000155721s
declaration order verified in 2.294e-06s
environment built in 2.3013e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00256602s wall (1.73698e-06 core-hours over 4 workers); 1 reduction steps; peak 18 MB in one worker

Test "tutorial/019_tut06_bad01"

Expected: ✋ reject · Size: 427 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 16 ms · instructions: 6.3 M · max rss memory: 21.7 MB

stderr:

loaded 1 declarations, 2 exprs (2 unique), 2 names in 0.000155201s
declaration order verified in 3.086e-06s
environment built in 1.7423e-05s; checking with 4 worker processes
FAIL tut06_bad01 (line 8): duplicate universe level parameter 'u'
checked 0 declarations, 1 failed, in 0.0026595s wall (1.40941e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/020_levelComp4"

Expected: 👍 accept · Size: 424 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 20 ms · instructions: 6.3 M · max rss memory: 21.8 MB

stderr:

loaded 1 declarations, 2 exprs (2 unique), 2 names in 8.9789e-05s
declaration order verified in 1.813e-06s
environment built in 1.5178e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00262633s wall (1.13007e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/021_levelComp5"

Expected: 👍 accept · Size: 424 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 15 ms · instructions: 6.3 M · max rss memory: 21.6 MB

stderr:

loaded 1 declarations, 2 exprs (2 unique), 2 names in 8.3928e-05s
declaration order verified in 4.448e-06s
environment built in 1.3716e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00187836s wall (1.24273e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/022_imax1"

Expected: 👍 accept · Size: 809 B · Lines: 16 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 16 ms · instructions: 6.3 M · max rss memory: 21.7 MB

stderr:

loaded 1 declarations, 6 exprs (6 unique), 7 names in 0.000116358s
declaration order verified in 2.114e-06s
environment built in 1.5739e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00220893s wall (1.40958e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/023_imax2"

Expected: 👍 accept · Size: 828 B · Lines: 17 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 15 ms · instructions: 6.3 M · max rss memory: 21.7 MB

stderr:

loaded 1 declarations, 6 exprs (6 unique), 7 names in 0.00011728s
declaration order verified in 6.312e-06s
environment built in 2.5217e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00224561s wall (1.4992e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/024_levelMaxComm"

Expected: 👍 accept · Size: 524 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 39 ms · instructions: 6.3 M · max rss memory: 21.7 MB

stderr:

loaded 1 declarations, 2 exprs (2 unique), 3 names in 0.000106419s
declaration order verified in 1.733e-06s
environment built in 2.5367e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00171172s wall (1.20906e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/025_levelMaxAssoc"

Expected: 👍 accept · Size: 623 B · Lines: 16 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 15 ms · instructions: 6.3 M · max rss memory: 21.5 MB

stderr:

loaded 1 declarations, 2 exprs (2 unique), 4 names in 9.7122e-05s
declaration order verified in 2.174e-06s
environment built in 1.5409e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00170326s wall (1.20222e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/026_levelMaxIdem"

Expected: 👍 accept · Size: 447 B · Lines: 9 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 14 ms · instructions: 6.3 M · max rss memory: 21.7 MB

stderr:

loaded 1 declarations, 2 exprs (2 unique), 2 names in 9.8975e-05s
declaration order verified in 1.643e-06s
environment built in 1.4867e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00151921s wall (9.18931e-07 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/027_levelMaxAbsorb"

Expected: 👍 accept · Size: 526 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 17 ms · instructions: 6.3 M · max rss memory: 21.5 MB

stderr:

loaded 1 declarations, 2 exprs (2 unique), 3 names in 0.000127349s
declaration order verified in 2.034e-06s
environment built in 1.9227e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00196111s wall (1.16807e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/028_inferVar"

Expected: 👍 accept · Size: 713 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 15 ms · instructions: 6.3 M · max rss memory: 21.7 MB

stderr:

loaded 1 declarations, 7 exprs (7 unique), 3 names in 0.000116589s
declaration order verified in 1.763e-06s
environment built in 1.6992e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00149809s wall (1.03156e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/029_defEqLambda"

Expected: 👍 accept · Size: 1.4 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 15 ms · instructions: 6.3 M · max rss memory: 21.6 MB

stderr:

loaded 1 declarations, 15 exprs (15 unique), 9 names in 0.000120206s
declaration order verified in 2.855e-06s
environment built in 1.6701e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00226392s wall (1.27353e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/030_peano1"

Expected: 👍 accept · Size: 3.6 KB · Lines: 73 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 17 ms · instructions: 6.6 M · max rss memory: 21.5 MB

stderr:

loaded 7 declarations, 41 exprs (41 unique), 20 names in 0.000100218s
declaration order verified in 6.572e-06s
environment built in 1.1892e-05s; checking with 4 worker processes
checked 7 declarations, 0 failed, in 0.00289688s wall (1.34893e-06 core-hours over 4 workers); 5 reduction steps; peak 18 MB in one worker

Test "tutorial/031_peano2"

Expected: 👍 accept · Size: 4.5 KB · Lines: 90 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 18 ms · instructions: 6.8 M · max rss memory: 21.8 MB

stderr:

loaded 8 declarations, 55 exprs (55 unique), 22 names in 0.000150492s
declaration order verified in 3.777e-06s
environment built in 1.8525e-05s; checking with 4 worker processes
checked 8 declarations, 0 failed, in 0.00281081s wall (1.98438e-06 core-hours over 4 workers); 23 reduction steps; peak 19 MB in one worker

Test "tutorial/032_peano3"

Expected: 👍 accept · Size: 4.9 KB · Lines: 98 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 19 ms · instructions: 6.9 M · max rss memory: 21.6 MB

stderr:

loaded 10 declarations, 59 exprs (59 unique), 24 names in 0.0001602s
declaration order verified in 3.967e-06s
environment built in 1.8345e-05s; checking with 4 worker processes
checked 10 declarations, 0 failed, in 0.00596075s wall (2.60671e-06 core-hours over 4 workers); 37 reduction steps; peak 19 MB in one worker

Test "tutorial/033_letType"

Expected: 👍 accept · Size: 489 B · Lines: 9 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 19 ms · instructions: 6.3 M · max rss memory: 21.7 MB

stderr:

loaded 1 declarations, 4 exprs (4 unique), 2 names in 0.000116198s
declaration order verified in 6.392e-06s
environment built in 2.3664e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00291896s wall (1.54866e-06 core-hours over 4 workers); 1 reduction steps; peak 18 MB in one worker

Test "tutorial/034_letTypeDep"

Expected: 👍 accept · Size: 1.2 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 18 ms · instructions: 6.3 M · max rss memory: 21.7 MB

stderr:

loaded 3 declarations, 11 exprs (11 unique), 10 names in 0.000157576s
declaration order verified in 1.984e-06s
environment built in 2.2712e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00273071s wall (1.42198e-06 core-hours over 4 workers); 1 reduction steps; peak 18 MB in one worker

Test "tutorial/035_letRed"

Expected: 👍 accept · Size: 627 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 16 ms · instructions: 6.3 M · max rss memory: 21.8 MB

stderr:

loaded 2 declarations, 5 exprs (5 unique), 3 names in 8.1974e-05s
declaration order verified in 1.653e-06s
environment built in 1.3706e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00180556s wall (1.09626e-06 core-hours over 4 workers); 4 reduction steps; peak 18 MB in one worker

Test "tutorial/036_empty"

Expected: 👍 accept · Size: 1.2 KB · Lines: 20 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 15 ms · instructions: 6.3 M · max rss memory: 21.8 MB

stderr:

loaded 2 declarations, 9 exprs (9 unique), 6 names in 0.000132829s
declaration order verified in 2.084e-06s
environment built in 2.4386e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00211136s wall (1.475e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/037_boolType"

Expected: 👍 accept · Size: 2.3 KB · Lines: 37 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 14 ms · instructions: 6.4 M · max rss memory: 21.5 MB

stderr:

loaded 2 declarations, 22 exprs (22 unique), 10 names in 0.000139261s
declaration order verified in 2.084e-06s
environment built in 1.2694e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00159517s wall (1.15055e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/038_twoBool"

Expected: 👍 accept · Size: 4.2 KB · Lines: 65 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 15 ms · instructions: 6.6 M · max rss memory: 21.6 MB

stderr:

loaded 3 declarations, 43 exprs (43 unique), 16 names in 0.000162665s
declaration order verified in 1.1572e-05s
environment built in 2.1571e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00236839s wall (1.42656e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/039_andType"

Expected: 👍 accept · Size: 3.2 KB · Lines: 57 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 17 ms · instructions: 6.6 M · max rss memory: 21.6 MB

stderr:

loaded 2 declarations, 41 exprs (41 unique), 12 names in 0.000116669s
declaration order verified in 4.358e-06s
environment built in 1.2053e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00229165s wall (1.58311e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/040_prodType"

Expected: 👍 accept · Size: 3.8 KB · Lines: 76 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 21 ms · instructions: 6.6 M · max rss memory: 21.9 MB

stderr:

loaded 2 declarations, 47 exprs (47 unique), 19 names in 0.000186399s
declaration order verified in 5.099e-06s
environment built in 1.6822e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00244291s wall (1.84701e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/041_pprodType"

Expected: 👍 accept · Size: 3.8 KB · Lines: 75 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 19 ms · instructions: 6.7 M · max rss memory: 21.7 MB

stderr:

loaded 2 declarations, 47 exprs (47 unique), 19 names in 0.000156213s
declaration order verified in 6.592e-06s
environment built in 2.3364e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.0023582s wall (1.60878e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/042_pUnitType"

Expected: 👍 accept · Size: 1.8 KB · Lines: 31 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 15 ms · instructions: 6.4 M · max rss memory: 21.7 MB

stderr:

loaded 2 declarations, 16 exprs (16 unique), 9 names in 0.000146295s
declaration order verified in 1.963e-06s
environment built in 1.4798e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00180897s wall (1.30472e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/043_eqType"

Expected: 👍 accept · Size: 3.2 KB · Lines: 62 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 16 ms · instructions: 6.6 M · max rss memory: 21.6 MB

stderr:

loaded 2 declarations, 42 exprs (42 unique), 15 names in 0.000165109s
declaration order verified in 9.688e-06s
environment built in 2.2813e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00231784s wall (1.58496e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/044_natDef"

Expected: 👍 accept · Size: 3.3 KB · Lines: 61 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 15 ms · instructions: 6.5 M · max rss memory: 21.8 MB

stderr:

loaded 2 declarations, 36 exprs (36 unique), 20 names in 0.000136496s
declaration order verified in 6.702e-06s
environment built in 1.3335e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00181884s wall (1.34547e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/045_rbTreeDef"

Expected: 👍 accept · Size: 15.7 KB · Lines: 296 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 20 ms · instructions: 8.9 M · max rss memory: 21.8 MB

stderr:

loaded 4 declarations, 248 exprs (248 unique), 39 names in 0.000678382s
declaration order verified in 2.715e-06s
environment built in 1.4147e-05s; checking with 4 worker processes
checked 4 declarations, 0 failed, in 0.00548872s wall (2.50261e-06 core-hours over 4 workers); 0 reduction steps; peak 21 MB in one worker

Test "tutorial/046_inductBadNonSort"

Expected: ✋ reject · Size: 1.2 KB · Lines: 20 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 16 ms · instructions: 6.4 M · max rss memory: 21.6 MB

stderr:

loaded 2 declarations, 7 exprs (7 unique), 9 names in 0.000123261s
declaration order verified in 2.274e-06s
environment built in 1.3856e-05s; checking with 4 worker processes
FAIL inductBadNonSort (line 20): type expected: constType
checked 1 declarations, 1 failed, in 0.0030023s wall (1.65404e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/047_inductBadNonSort2"

Expected: ✋ reject · Size: 598 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 17 ms · instructions: 6.3 M · max rss memory: 21.7 MB

stderr:

loaded 2 declarations, 2 exprs (2 unique), 2 names in 0.000125415s
declaration order verified in 2.174e-06s
environment built in 1.7743e-05s; checking with 4 worker processes
FAIL inductBadNonSort2 (line 8): type expected: aType
checked 1 declarations, 1 failed, in 0.0022607s wall (1.52322e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/048_inductLevelParam"

Expected: ✋ reject · Size: 515 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 17 ms · instructions: 6.3 M · max rss memory: 21.6 MB

stderr:

loaded 1 declarations, 1 exprs (1 unique), 2 names in 0.000125706s
declaration order verified in 1.834e-06s
environment built in 2.4106e-05s; checking with 4 worker processes
FAIL inductLevelParam (line 7): duplicate universe level parameter 'u'
checked 0 declarations, 1 failed, in 0.00185063s wall (1.25728e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/049_inductTooFewParams"

Expected: ✋ reject · Size: 548 B · Lines: 6 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 30 ms · instructions: 6.3 M · max rss memory: 21.6 MB

stderr:

loaded 1 declarations, 2 exprs (2 unique), 2 names in 9.5369e-05s
declaration order verified in 2.034e-06s
environment built in 1.4757e-05s; checking with 4 worker processes
FAIL inductTooFewParams (line 6): invalid inductive datatype declaration, incorrect number of parameters
checked 0 declarations, 1 failed, in 0.00212265s wall (1.27069e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/050_inductWrongCtorParams"

Expected: ✋ reject · Size: 1.2 KB · Lines: 16 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 15 ms · instructions: 6.4 M · max rss memory: 21.7 MB

stderr:

loaded 2 declarations, 7 exprs (7 unique), 5 names in 0.000115376s
declaration order verified in 1.813e-06s
environment built in 1.9066e-05s; checking with 4 worker processes
FAIL inductWrongCtorParams (line 16): arg #1 of 'inductWrongCtorParams.mk' does not match inductive datatype parameters
checked 1 declarations, 1 failed, in 0.00220315s wall (1.18153e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/051_inductWrongCtorResParams"

Expected: ✋ reject · Size: 1.3 KB · Lines: 19 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 15 ms · instructions: 6.4 M · max rss memory: 21.6 MB

stderr:

loaded 1 declarations, 11 exprs (11 unique), 5 names in 0.000104907s
declaration order verified in 6.162e-06s
environment built in 1.3596e-05s; checking with 4 worker processes
FAIL inductWrongCtorResParams (line 19): invalid return type for 'inductWrongCtorResParams.mk'
checked 0 declarations, 1 failed, in 0.00199047s wall (1.44233e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/052_inductWrongCtorResLevel"

Expected: ✋ reject · Size: 1.4 KB · Lines: 23 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 19 ms · instructions: 6.4 M · max rss memory: 21.7 MB

stderr:

loaded 1 declarations, 11 exprs (11 unique), 7 names in 0.000135745s
declaration order verified in 2.374e-06s
environment built in 3.4124e-05s; checking with 4 worker processes
FAIL inductWrongCtorResLevel (line 23): invalid return type for 'inductWrongCtorResLevel.mk'
checked 0 declarations, 1 failed, in 0.00312091s wall (1.71068e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/053_inductInIndex"

Expected: ✋ reject · Size: 1.1 KB · Lines: 14 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 18 ms · instructions: 6.4 M · max rss memory: 21.9 MB

stderr:

loaded 2 declarations, 6 exprs (6 unique), 5 names in 0.000280586s
declaration order verified in 7.905e-06s
environment built in 2.4015e-05s; checking with 4 worker processes
FAIL inductInIndex (line 14): invalid return type for 'inductInIndex.mk'
checked 1 declarations, 1 failed, in 0.00243762s wall (1.63438e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/054_indNeg"

Expected: ✋ reject · Size: 996 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 17 ms · instructions: 6.4 M · max rss memory: 21.7 MB

stderr:

loaded 1 declarations, 5 exprs (5 unique), 4 names in 0.000130945s
declaration order verified in 5.19e-06s
environment built in 1.6481e-05s; checking with 4 worker processes
FAIL indNeg (line 12): arg #1 of 'indNeg.mk' has a non positive occurrence of the datatypes being declared
checked 0 declarations, 1 failed, in 0.00256009s wall (1.49983e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/055_reduceCtorParam.mk"

Expected: 👍 accept · Size: 4.1 KB · Lines: 80 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 18 ms · instructions: 6.8 M · max rss memory: 21.5 MB

stderr:

loaded 3 declarations, 54 exprs (54 unique), 18 names in 0.000168706s
declaration order verified in 4.759e-06s
environment built in 2.4697e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00251251s wall (2.00965e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/056_reduceCtorType.mk"

Expected: ✋ reject · Size: 1.5 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 16 ms · instructions: 6.5 M · max rss memory: 21.6 MB

stderr:

loaded 2 declarations, 13 exprs (13 unique), 7 names in 0.000142087s
declaration order verified in 2.585e-06s
environment built in 1.6641e-05s; checking with 4 worker processes
FAIL reduceCtorType (line 26): invalid return type for 'reduceCtorType.mk'
checked 1 declarations, 1 failed, in 0.00217717s wall (1.25212e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/057_indNegReducible"

Expected: ✋ reject · Size: 1.9 KB · Lines: 31 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 20 ms · instructions: 6.4 M · max rss memory: 21.5 MB

stderr:

loaded 3 declarations, 14 exprs (14 unique), 12 names in 0.000130936s
declaration order verified in 2.495e-06s
environment built in 2.2723e-05s; checking with 4 worker processes
FAIL indNegReducible (line 31): arg #1 of 'indNegReducible.mk' has a non positive occurrence of the datatypes being declared
checked 2 declarations, 1 failed, in 0.00260607s wall (1.34912e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/058_predWithTypeField"

Expected: 👍 accept · Size: 2.0 KB · Lines: 32 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 17 ms · instructions: 6.4 M · max rss memory: 21.7 MB

stderr:

loaded 2 declarations, 20 exprs (20 unique), 8 names in 0.000113994s
declaration order verified in 1.713e-06s
environment built in 1.2894e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00227471s wall (1.32366e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/059_typeWithTypeField"

Expected: 👍 accept · Size: 2.1 KB · Lines: 36 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 16 ms · instructions: 6.4 M · max rss memory: 21.6 MB

stderr:

loaded 2 declarations, 21 exprs (21 unique), 9 names in 0.000145162s
declaration order verified in 1.964e-06s
environment built in 1.3486e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00231049s wall (1.29383e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/060_typeWithTypeFieldPoly"

Expected: 👍 accept · Size: 2.1 KB · Lines: 38 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 16 ms · instructions: 6.4 M · max rss memory: 21.5 MB

stderr:

loaded 2 declarations, 21 exprs (21 unique), 10 names in 0.000139151s
declaration order verified in 1.833e-06s
environment built in 1.2744e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00267217s wall (1.52963e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/061_typeWithTooHighTypeField.mk"

Expected: ✋ reject · Size: 943 B · Lines: 11 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 19 ms · instructions: 6.4 M · max rss memory: 21.6 MB

stderr:

loaded 1 declarations, 4 exprs (4 unique), 4 names in 8.8977e-05s
declaration order verified in 4.559e-06s
environment built in 1.0489e-05s; checking with 4 worker processes
FAIL typeWithTooHighTypeField (line 11): universe level of type_of(arg #1) of 'typeWithTooHighTypeField.mk' is too big for the corresponding inductive datatype
checked 0 declarations, 1 failed, in 0.00284071s wall (1.14467e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/062_emptyRec"

Expected: 👍 accept · Size: 1.2 KB · Lines: 21 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 16 ms · instructions: 6.4 M · max rss memory: 21.7 MB

stderr:

loaded 2 declarations, 10 exprs (10 unique), 6 names in 0.000124433s
declaration order verified in 2.304e-06s
environment built in 2.0529e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00239781s wall (1.27674e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/063_boolRec"

Expected: 👍 accept · Size: 3.0 KB · Lines: 53 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 15 ms · instructions: 6.5 M · max rss memory: 21.5 MB

stderr:

loaded 2 declarations, 32 exprs (32 unique), 16 names in 0.000129873s
declaration order verified in 6.652e-06s
environment built in 1.4547e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00228775s wall (1.34805e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/064_twoBoolRec"

Expected: 👍 accept · Size: 4.8 KB · Lines: 78 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 15 ms · instructions: 6.7 M · max rss memory: 21.7 MB

stderr:

loaded 3 declarations, 50 exprs (50 unique), 22 names in 0.000194013s
declaration order verified in 0.000103764s
environment built in 2.665e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00241463s wall (1.49711e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/065_andRec"

Expected: 👍 accept · Size: 3.2 KB · Lines: 58 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 17 ms · instructions: 6.7 M · max rss memory: 21.6 MB

stderr:

loaded 2 declarations, 42 exprs (42 unique), 12 names in 0.000142106s
declaration order verified in 3.777e-06s
environment built in 1.3425e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00261673s wall (1.88018e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/066_prodRec"

Expected: 👍 accept · Size: 4.0 KB · Lines: 79 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 16 ms · instructions: 6.7 M · max rss memory: 21.6 MB

stderr:

loaded 2 declarations, 49 exprs (49 unique), 20 names in 0.000120376s
declaration order verified in 4.038e-06s
environment built in 2.0839e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00255551s wall (1.98724e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/067_pprodRec"

Expected: 👍 accept · Size: 4.0 KB · Lines: 78 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 14 ms · instructions: 6.7 M · max rss memory: 21.8 MB

stderr:

loaded 2 declarations, 48 exprs (48 unique), 20 names in 0.000129142s
declaration order verified in 4.068e-06s
environment built in 1.9566e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00203678s wall (1.65542e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/068_punitRec"

Expected: 👍 accept · Size: 2.2 KB · Lines: 39 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 15 ms · instructions: 6.4 M · max rss memory: 21.5 MB

stderr:

loaded 2 declarations, 18 exprs (18 unique), 15 names in 0.000103404s
declaration order verified in 1.764e-06s
environment built in 2.2172e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00171418s wall (1.24907e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/069_eqRec"

Expected: 👍 accept · Size: 3.3 KB · Lines: 63 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 15 ms · instructions: 6.7 M · max rss memory: 21.7 MB

stderr:

loaded 2 declarations, 43 exprs (43 unique), 15 names in 0.000146034s
declaration order verified in 6.613e-06s
environment built in 2.3344e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00237494s wall (1.61585e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/070_nRec"

Expected: 👍 accept · Size: 3.3 KB · Lines: 61 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 15 ms · instructions: 6.6 M · max rss memory: 21.6 MB

stderr:

loaded 2 declarations, 36 exprs (36 unique), 20 names in 0.000118943s
declaration order verified in 6.823e-06s
environment built in 1.2694e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00232006s wall (1.37104e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/071_rbTreeRef"

Expected: 👍 accept · Size: 16.2 KB · Lines: 303 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 19 ms · instructions: 9.2 M · max rss memory: 21.4 MB

stderr:

loaded 4 declarations, 254 exprs (254 unique), 40 names in 0.000920587s
declaration order verified in 5.059e-06s
environment built in 2.1099e-05s; checking with 4 worker processes
checked 4 declarations, 0 failed, in 0.00591282s wall (3.34841e-06 core-hours over 4 workers); 0 reduction steps; peak 20 MB in one worker

Test "tutorial/072_boolPropRec"

Expected: 👍 accept · Size: 2.3 KB · Lines: 34 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 38 ms · instructions: 6.4 M · max rss memory: 21.8 MB

stderr:

loaded 2 declarations, 22 exprs (22 unique), 9 names in 0.000119023s
declaration order verified in 4.278e-06s
environment built in 1.5389e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00205467s wall (1.54827e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/073_BogusRecursor"

Expected: ✋ reject · Size: 1.8 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

inductive BogusRecursor : Type where
  | mk : BogusRecursor

Test result: ✋ rejected · exit code 1 · wall time: 16 ms · instructions: 6.5 M · max rss memory: 21.7 MB

stderr:

loaded 3 declarations, 12 exprs (12 unique), 9 names in 0.000132217s
declaration order verified in 2.064e-06s
environment built in 1.3595e-05s; checking with 4 worker processes
FAIL BogusRecursor (line 24): recursor 'BogusRecursor.rec': parameter/index/motive/minor/K data differs from the derived recursor
checked 1 declarations, 1 failed, in 0.00296412s wall (1.90577e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/074_existsRec"

Expected: 👍 accept · Size: 3.6 KB · Lines: 66 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 17 ms · instructions: 6.8 M · max rss memory: 21.6 MB

stderr:

loaded 2 declarations, 45 exprs (45 unique), 17 names in 0.000168245s
declaration order verified in 3.817e-06s
environment built in 1.7092e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00303733s wall (2.14123e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/075_typeSingletonRecReduction"

Expected: 👍 accept · Size: 7.9 KB · Lines: 138 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 16 ms · instructions: 7.1 M · max rss memory: 21.6 MB

stderr:

loaded 5 declarations, 95 exprs (95 unique), 34 names in 0.000131406s
declaration order verified in 2.064e-06s
environment built in 1.3275e-05s; checking with 4 worker processes
checked 5 declarations, 0 failed, in 0.00288576s wall (2.07002e-06 core-hours over 4 workers); 5 reduction steps; peak 19 MB in one worker

Test "tutorial/076_sortElimPropRec"

Expected: 👍 accept · Size: 5.6 KB · Lines: 97 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 19 ms · instructions: 7.0 M · max rss memory: 21.6 MB

stderr:

loaded 3 declarations, 69 exprs (69 unique), 22 names in 0.000254577s
declaration order verified in 2.815e-06s
environment built in 2.2322e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00321706s wall (2.58134e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/077_sortElimProp2Rec"

Expected: 👍 accept · Size: 6.6 KB · Lines: 114 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 18 ms · instructions: 7.1 M · max rss memory: 21.6 MB

stderr:

loaded 4 declarations, 83 exprs (83 unique), 24 names in 0.000150352s
declaration order verified in 4.889e-06s
environment built in 2.2433e-05s; checking with 4 worker processes
checked 4 declarations, 0 failed, in 0.00278914s wall (1.96007e-06 core-hours over 4 workers); 2 reduction steps; peak 19 MB in one worker

Test "tutorial/078_boolRecEqns"

Expected: 👍 accept · Size: 10.8 KB · Lines: 199 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 17 ms · instructions: 7.5 M · max rss memory: 21.5 MB

stderr:

loaded 4 declarations, 133 exprs (133 unique), 58 names in 0.000479379s
declaration order verified in 2.956e-06s
environment built in 1.9897e-05s; checking with 4 worker processes
checked 4 declarations, 0 failed, in 0.00343281s wall (2.26904e-06 core-hours over 4 workers); 16 reduction steps; peak 19 MB in one worker

Test "tutorial/079_prodRecEqns"

Expected: 👍 accept · Size: 10.1 KB · Lines: 205 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 21 ms · instructions: 7.5 M · max rss memory: 21.8 MB

stderr:

loaded 3 declarations, 127 exprs (127 unique), 67 names in 0.000939601s
declaration order verified in 2.465e-06s
environment built in 1.3706e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00678455s wall (2.65875e-06 core-hours over 4 workers); 6 reduction steps; peak 20 MB in one worker

Test "tutorial/080_nRecReduction"

Expected: 👍 accept · Size: 12.7 KB · Lines: 238 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 18 ms · instructions: 7.7 M · max rss memory: 21.6 MB

stderr:

loaded 6 declarations, 170 exprs (170 unique), 58 names in 0.000387807s
declaration order verified in 3.246e-06s
environment built in 2.112e-05s; checking with 4 worker processes
checked 6 declarations, 0 failed, in 0.00402407s wall (2.3964e-06 core-hours over 4 workers); 43 reduction steps; peak 20 MB in one worker

Test "tutorial/081_listRecReduction"

Expected: 👍 accept · Size: 17.5 KB · Lines: 335 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 19 ms · instructions: 8.9 M · max rss memory: 21.8 MB

stderr:

loaded 7 declarations, 256 exprs (256 unique), 67 names in 0.000525816s
declaration order verified in 4.479e-06s
environment built in 6.3038e-05s; checking with 4 worker processes
checked 7 declarations, 0 failed, in 0.00532993s wall (3.09673e-06 core-hours over 4 workers); 44 reduction steps; peak 21 MB in one worker

Test "tutorial/082_RBTree.id_spec"

Expected: 👍 accept · Size: 47.9 KB · Lines: 1.0 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 21 ms · instructions: 15.5 M · max rss memory: 22.3 MB

stderr:

loaded 7 declarations, 878 exprs (878 unique), 116 names in 0.000542567s
declaration order verified in 5.791e-06s
environment built in 1.7774e-05s; checking with 4 worker processes
checked 7 declarations, 0 failed, in 0.007435s wall (4.94787e-06 core-hours over 4 workers); 46 reduction steps; peak 22 MB in one worker

Test "tutorial/083_And.right"

Expected: 👍 accept · Size: 4.3 KB · Lines: 74 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 16 ms · instructions: 6.7 M · max rss memory: 21.6 MB

stderr:

loaded 3 declarations, 55 exprs (55 unique), 14 names in 0.00015999s
declaration order verified in 3.878e-06s
environment built in 1.6572e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.002278s wall (1.84877e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/084_Prod.snd"

Expected: 👍 accept · Size: 4.5 KB · Lines: 83 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 17 ms · instructions: 6.8 M · max rss memory: 21.6 MB

stderr:

loaded 3 declarations, 57 exprs (57 unique), 16 names in 0.000194725s
declaration order verified in 4.258e-06s
environment built in 1.7793e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00302653s wall (1.97879e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/085_PProd.snd"

Expected: 👍 accept · Size: 4.5 KB · Lines: 83 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 16 ms · instructions: 6.8 M · max rss memory: 21.6 MB

stderr:

loaded 3 declarations, 57 exprs (57 unique), 16 names in 0.000113112s
declaration order verified in 3.456e-06s
environment built in 1.7183e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00227825s wall (1.50842e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/086_PSigma.snd"

Expected: 👍 accept · Size: 5.1 KB · Lines: 96 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 21 ms · instructions: 7.0 M · max rss memory: 21.7 MB

stderr:

loaded 3 declarations, 65 exprs (65 unique), 21 names in 0.000151715s
declaration order verified in 3.135e-06s
environment built in 2.3013e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.0040087s wall (2.28143e-06 core-hours over 4 workers); 1 reduction steps; peak 19 MB in one worker

Test "tutorial/087_projOutOfRange"

Expected: ✋ reject · Size: 3.8 KB · Lines: 67 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 17 ms · instructions: 6.7 M · max rss memory: 21.8 MB

stderr:

loaded 2 declarations, 48 exprs (48 unique), 15 names in 0.000166432s
declaration order verified in 3.667e-06s
environment built in 2.5808e-05s; checking with 4 worker processes
FAIL projOutOfRange (line 67): invalid projection And.2
checked 1 declarations, 1 failed, in 0.00276974s wall (1.61615e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/088_projNotStruct"

Expected: ✋ reject · Size: 3.5 KB · Lines: 64 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 20 ms · instructions: 6.6 M · max rss memory: 21.7 MB

stderr:

loaded 2 declarations, 38 exprs (38 unique), 21 names in 0.000308909s
declaration order verified in 7.414e-06s
environment built in 2.4416e-05s; checking with 4 worker processes
FAIL projNotStruct (line 64): invalid projection N.0
checked 1 declarations, 1 failed, in 0.0042374s wall (3.60477e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/089_projProp1"

Expected: 👍 accept · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 21 ms · instructions: 7.1 M · max rss memory: 21.7 MB

stderr:

loaded 4 declarations, 103 exprs (103 unique), 31 names in 0.000383599s
declaration order verified in 3.396e-06s
environment built in 2.0268e-05s; checking with 4 worker processes
checked 4 declarations, 0 failed, in 0.0032334s wall (2.10642e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/090_projProp2"

Expected: ✋ reject · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 17 ms · instructions: 7.2 M · max rss memory: 21.6 MB

stderr:

loaded 4 declarations, 103 exprs (103 unique), 31 names in 0.000302377s
declaration order verified in 2.324e-06s
environment built in 2.2292e-05s; checking with 4 worker processes
FAIL projProp2 (line 143): invalid projection PropStructure.1
checked 3 declarations, 1 failed, in 0.00241871s wall (1.77601e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/091_projProp3"

Expected: 👍 accept · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 16 ms · instructions: 7.1 M · max rss memory: 21.7 MB

stderr:

loaded 4 declarations, 103 exprs (103 unique), 31 names in 0.000347662s
declaration order verified in 2.385e-06s
environment built in 1.4026e-05s; checking with 4 worker processes
checked 4 declarations, 0 failed, in 0.0022923s wall (1.78498e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/092_projProp4"

Expected: ✋ reject · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 15 ms · instructions: 7.2 M · max rss memory: 21.7 MB

stderr:

loaded 4 declarations, 103 exprs (103 unique), 31 names in 0.00026622s
declaration order verified in 2.285e-06s
environment built in 1.4226e-05s; checking with 4 worker processes
FAIL projProp4 (line 143): invalid projection PropStructure.3
checked 3 declarations, 1 failed, in 0.00201607s wall (1.45956e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/093_projProp5"

Expected: ✋ reject · Size: 8.4 KB · Lines: 148 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 15 ms · instructions: 7.2 M · max rss memory: 21.7 MB

stderr:

loaded 4 declarations, 108 exprs (108 unique), 31 names in 0.000251351s
declaration order verified in 2.354e-06s
environment built in 1.2172e-05s; checking with 4 worker processes
FAIL projProp5 (line 148): invalid projection PropStructure.3
checked 3 declarations, 1 failed, in 0.00204538s wall (1.39253e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/094_projProp6"

Expected: ✋ reject · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 17 ms · instructions: 7.2 M · max rss memory: 21.7 MB

stderr:

loaded 4 declarations, 103 exprs (103 unique), 31 names in 0.000348824s
declaration order verified in 2.394e-06s
environment built in 1.8364e-05s; checking with 4 worker processes
FAIL projProp6 (line 143): invalid projection PropStructure.5
checked 3 declarations, 1 failed, in 0.00325344s wall (1.8581e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/095_projDataIndexRec"

Expected: 👍 accept · Size: 6.8 KB · Lines: 111 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 16 ms · instructions: 6.9 M · max rss memory: 21.8 MB

stderr:

loaded 4 declarations, 72 exprs (72 unique), 31 names in 0.000173325s
declaration order verified in 2.114e-06s
environment built in 2.6008e-05s; checking with 4 worker processes
checked 4 declarations, 0 failed, in 0.00236779s wall (1.60757e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/096_projIndexData"

Expected: ✋ reject · Size: 14.1 KB · Lines: 226 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 18 ms · instructions: 7.8 M · max rss memory: 21.6 MB

stderr:

loaded 7 declarations, 163 exprs (163 unique), 51 names in 0.000366347s
declaration order verified in 2.434e-06s
environment built in 2.2933e-05s; checking with 4 worker processes
FAIL projIndexData (line 226): invalid projection PropStructure.0
checked 6 declarations, 1 failed, in 0.00328808s wall (2.43791e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/097_projIndexData2"

Expected: ✋ reject · Size: 14.1 KB · Lines: 226 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 17 ms · instructions: 7.8 M · max rss memory: 21.6 MB

stderr:

loaded 7 declarations, 163 exprs (163 unique), 51 names in 0.000377027s
declaration order verified in 2.405e-06s
environment built in 1.7663e-05s; checking with 4 worker processes
FAIL projIndexData2 (line 226): invalid projection PropStructure.1
checked 6 declarations, 1 failed, in 0.00268228s wall (2.04677e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/098_projRed"

Expected: 👍 accept · Size: 9.9 KB · Lines: 177 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 18 ms · instructions: 7.4 M · max rss memory: 21.8 MB

stderr:

loaded 6 declarations, 131 exprs (131 unique), 32 names in 0.00068831s
declaration order verified in 3.616e-06s
environment built in 1.8695e-05s; checking with 4 worker processes
checked 6 declarations, 0 failed, in 0.00267865s wall (2.27351e-06 core-hours over 4 workers); 2 reduction steps; peak 19 MB in one worker

Test "tutorial/099_ruleK"

Expected: 👍 accept · Size: 6.5 KB · Lines: 121 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 18 ms · instructions: 7.0 M · max rss memory: 21.8 MB

stderr:

loaded 3 declarations, 83 exprs (83 unique), 31 names in 0.000180378s
declaration order verified in 2.104e-06s
environment built in 2.3905e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00324191s wall (2.21334e-06 core-hours over 4 workers); 4 reduction steps; peak 19 MB in one worker

Test "tutorial/100_ruleKbad"

Expected: ✋ reject · Size: 6.5 KB · Lines: 121 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 18 ms · instructions: 7.1 M · max rss memory: 21.6 MB

stderr:

loaded 3 declarations, 83 exprs (83 unique), 31 names in 0.00015958s
declaration order verified in 4.749e-06s
environment built in 2.5428e-05s; checking with 4 worker processes
FAIL ruleKbad (line 121): declaration type mismatch for 'ruleKbad'
  inferred: ((x._@.Tutorial.3161876795._hygCtx._hyg.27 : (((Eq.{1} Bool) Bool.true) Bool.false)) -> ((a : Bool) -> (((Eq.{1} Bool) #0) #0)))
  declared: ((h : (((Eq.{1} Bool) Bool.true) Bool.false)) -> ((a : Bool) -> (((Eq.{1} Bool) ((((((Eq.rec.{1, 1} Bool) Bool.true) (fun (x._@.Tutorial.3161876795._hygCtx._hyg.17 : Bool) => (fun (x._@.Tutorial.3161876795._hygCtx._hyg.19 : (((Eq.{1} Bool) Bool.true) #0)) => Bool))) #0) Bool.false) #1)) #0)))
checked 2 declarations, 1 failed, in 0.00314128s wall (1.89079e-06 core-hours over 4 workers); 0 reduction steps; peak 20 MB in one worker

Test "tutorial/101_ruleKAcc"

Expected: ✋ reject · Size: 12.5 KB · Lines: 229 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 19 ms · instructions: 8.2 M · max rss memory: 21.5 MB

stderr:

loaded 4 declarations, 180 exprs (180 unique), 41 names in 0.00038914s
declaration order verified in 3.066e-06s
environment built in 1.2684e-05s; checking with 4 worker processes
FAIL ruleKAcc (line 229): declaration type mismatch for 'ruleKAcc'
  inferred: ((α : Sort(u)) -> ((p : ((a._@._internal._hyg.0 : #0) -> ((a._@._internal._hyg.0 : #1) -> Sort(0)))) -> ((x : #1) -> ((h : (((Acc.{u} #2) #1) #0)) -> ((a : Bool) -> (((Eq.{1} Bool) #0) #0))))))
  declared: ((α : Sort(u)) -> ((p : ((a._@._internal._hyg.0 : #0) -> ((a._@._internal._hyg.0 : #1) -> Sort(0)))) -> ((x : #1) -> ((h : (((Acc.{u} #2) #1) #0)) -> ((a : Bool) -> (((Eq.{1} Bool) ((((((Acc.rec.{1, u} #4) #3) (fun (x._@.Tutorial.4255978773._hygCtx._hyg.22 : #4) => (fun (x._@.Tutorial.4255978773._hygCtx._hyg.24 : (((Acc.{u} #5) #4) #0)) => Bool))) (fun (x._@.Tutorial.4255978773._hygCtx._hyg.31 : #4) => (fun (x._@.Tutorial.4255978773._hygCtx._hyg.33 : ((y : #5) -> ((a._@._internal._hyg.0 : ((#5 #0) #1)) -> (((Acc.{u} #7) #6) #1)))) => (fun (x._@.Tutorial.4255978773._hygCtx._hyg.35 : ((y : #6) -> ((a._@._internal._hyg.0 : ((#6 #0) #2)) -> Bool))) => #3)))) #2) #1)) #0))))))
checked 3 declarations, 1 failed, in 0.00481265s wall (2.69291e-06 core-hours over 4 workers); 0 reduction steps; peak 21 MB in one worker

Test "tutorial/102_aNatLit"

Expected: 👍 accept · Size: 3.0 KB · Lines: 54 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 16 ms · instructions: 6.5 M · max rss memory: 21.8 MB

stderr:

loaded 2 declarations, 37 exprs (37 unique), 12 names in 0.000113813s
declaration order verified in 3.536e-06s
environment built in 1.3125e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00214809s wall (1.35301e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/103_natLitEq"

Expected: 👍 accept · Size: 6.1 KB · Lines: 114 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 16 ms · instructions: 7.0 M · max rss memory: 21.8 MB

stderr:

loaded 3 declarations, 84 exprs (84 unique), 23 names in 0.000163948s
declaration order verified in 9.107e-06s
environment built in 2.3574e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00252433s wall (2.20729e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/104_proofIrrelevance"

Expected: 👍 accept · Size: 5.0 KB · Lines: 100 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 14 ms · instructions: 6.8 M · max rss memory: 21.6 MB

stderr:

loaded 3 declarations, 66 exprs (66 unique), 28 names in 9.8785e-05s
declaration order verified in 1.974e-06s
environment built in 1.7844e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00207827s wall (1.26443e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/105_proofIrrelevanceBad"

Expected: ✋ reject · Size: 4.7 KB · Lines: 93 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 17 ms · instructions: 6.8 M · max rss memory: 21.7 MB

stderr:

loaded 3 declarations, 67 exprs (67 unique), 19 names in 9.8495e-05s
declaration order verified in 5.871e-06s
environment built in 1.4457e-05s; checking with 4 worker processes
FAIL proofIrrelevanceBad (line 93): declaration type mismatch for 'proofIrrelevanceBad'
  inferred: ((p : Sort(1)) -> ((h1 : #0) -> ((h2 : #1) -> (((Eq.{1} #2) #1) #1))))
  declared: ((p : Sort(1)) -> ((h1 : #0) -> ((h2 : #1) -> (((Eq.{1} #2) #1) #0))))
checked 2 declarations, 1 failed, in 0.00315429s wall (2.1062e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/106_proofIrrelevanceWhnf"

Expected: 👍 accept · Size: 5.6 KB · Lines: 112 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 15 ms · instructions: 6.9 M · max rss memory: 21.7 MB

stderr:

loaded 4 declarations, 74 exprs (74 unique), 29 names in 0.000137468s
declaration order verified in 2.485e-06s
environment built in 1.6781e-05s; checking with 4 worker processes
checked 4 declarations, 0 failed, in 0.00252246s wall (1.56753e-06 core-hours over 4 workers); 10 reduction steps; peak 19 MB in one worker

Test "tutorial/107_proofIrrelevanceUnderBinder"

Expected: 👍 accept · Size: 1.9 KB · Lines: 39 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 14 ms · instructions: 6.4 M · max rss memory: 21.9 MB

stderr:

loaded 7 declarations, 17 exprs (17 unique), 13 names in 0.000135173s
declaration order verified in 5.681e-06s
environment built in 2.1029e-05s; checking with 4 worker processes
checked 7 declarations, 0 failed, in 0.00223086s wall (1.35923e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/108_unitEta1"

Expected: 👍 accept · Size: 6.2 KB · Lines: 116 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 6.9 M · max rss memory: 21.7 MB

stderr:

loaded 5 declarations, 77 exprs (77 unique), 30 names in 0.00014405s
declaration order verified in 2.014e-06s
environment built in 3.9464e-05s; checking with 4 worker processes
checked 5 declarations, 0 failed, in 0.00179044s wall (1.40336e-06 core-hours over 4 workers); 4 reduction steps; peak 19 MB in one worker

Test "tutorial/109_unitEta2"

Expected: 👍 accept · Size: 5.9 KB · Lines: 109 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 14 ms · instructions: 6.9 M · max rss memory: 21.6 MB

stderr:

loaded 4 declarations, 73 exprs (73 unique), 29 names in 0.000179747s
declaration order verified in 6.252e-06s
environment built in 1.5709e-05s; checking with 4 worker processes
checked 4 declarations, 0 failed, in 0.00206854s wall (1.6182e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/110_unitEta3"

Expected: 👍 accept · Size: 6.0 KB · Lines: 111 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 15 ms · instructions: 6.9 M · max rss memory: 21.6 MB

stderr:

loaded 4 declarations, 75 exprs (75 unique), 29 names in 0.000113784s
declaration order verified in 2.004e-06s
environment built in 1.5699e-05s; checking with 4 worker processes
checked 4 declarations, 0 failed, in 0.00186466s wall (1.34696e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/111_indexedUnitEta"

Expected: ✋ reject · Size: 7.2 KB · Lines: 121 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 15 ms · instructions: 7.1 M · max rss memory: 21.7 MB

stderr:

loaded 4 declarations, 86 exprs (86 unique), 27 names in 0.000126226s
declaration order verified in 2.124e-06s
environment built in 1.2944e-05s; checking with 4 worker processes
FAIL indexedUnitEta (line 121): declaration type mismatch for 'indexedUnitEta'
  inferred: ((x : (IndexedUnit Bool.true)) -> ((y : (IndexedUnit Bool.true)) -> (((Eq.{1} (IndexedUnit Bool.true)) #1) #1)))
  declared: ((x : (IndexedUnit Bool.true)) -> ((y : (IndexedUnit Bool.true)) -> (((Eq.{1} (IndexedUnit Bool.true)) #1) #0)))
checked 3 declarations, 1 failed, in 0.0022743s wall (1.67317e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/112_structEta"

Expected: 👍 accept · Size: 12.5 KB · Lines: 230 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 19 ms · instructions: 7.9 M · max rss memory: 21.7 MB

stderr:

loaded 7 declarations, 173 exprs (173 unique), 43 names in 0.000369493s
declaration order verified in 2.736e-06s
environment built in 6.1024e-05s; checking with 4 worker processes
checked 7 declarations, 0 failed, in 0.00442025s wall (3.12704e-06 core-hours over 4 workers); 4 reduction steps; peak 19 MB in one worker

Test "tutorial/113_indexedStructEta"

Expected: ✋ reject · Size: 8.5 KB · Lines: 138 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 18 ms · instructions: 7.2 M · max rss memory: 21.6 MB

stderr:

loaded 5 declarations, 99 exprs (99 unique), 30 names in 0.000365736s
declaration order verified in 2.816e-06s
environment built in 3.1328e-05s; checking with 4 worker processes
FAIL indexedStructEta (line 138): declaration type mismatch for 'indexedStructEta'
  inferred: ((a : (IndexedSingleton Bool.true)) -> (((Eq.{1} (IndexedSingleton Bool.true)) #0) #0))
  declared: ((x : (IndexedSingleton Bool.true)) -> (((Eq.{1} (IndexedSingleton Bool.true)) (IndexedSingleton.mk True.intro)) #0))
checked 4 declarations, 1 failed, in 0.0030865s wall (2.30698e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/114_funEta"

Expected: 👍 accept · Size: 5.2 KB · Lines: 104 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 18 ms · instructions: 6.8 M · max rss memory: 21.6 MB

stderr:

loaded 3 declarations, 71 exprs (71 unique), 26 names in 0.000188233s
declaration order verified in 2.645e-06s
environment built in 1.6201e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00270154s wall (2.20476e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/115_funEtaDep"

Expected: 👍 accept · Size: 5.3 KB · Lines: 106 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 17 ms · instructions: 6.9 M · max rss memory: 21.5 MB

stderr:

loaded 3 declarations, 73 exprs (73 unique), 26 names in 0.000201387s
declaration order verified in 8.476e-06s
environment built in 1.6792e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.0026762s wall (2.00873e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/116_funEtaBad"

Expected: ✋ reject · Size: 4.9 KB · Lines: 97 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 17 ms · instructions: 6.9 M · max rss memory: 21.5 MB

stderr:

loaded 2 declarations, 64 exprs (64 unique), 27 names in 0.000201408s
declaration order verified in 1.2884e-05s
environment built in 3.7931e-05s; checking with 4 worker processes
FAIL funEtaBad (line 97): declaration type mismatch for 'funEtaBad'
  inferred: ((x._@.Tutorial.4249243883._hygCtx._hyg.28 : Sort(1)) -> ((x._@.Tutorial.4249243883._hygCtx._hyg.30 : Sort(1)) -> ((x._@.Tutorial.4249243883._hygCtx._hyg.32 : ((a._@._internal._hyg.0 : #1) -> #2)) -> ((f : ((a._@._internal._hyg.0 : #2) -> #2)) -> (((Eq.{1} ((x : #3) -> #3)) #0) #0)))))
  declared: ((α : Sort(1)) -> ((β : Sort(1)) -> ((g : ((a._@._internal._hyg.0 : #1) -> #2)) -> ((f : ((a._@._internal._hyg.0 : #2) -> #2)) -> (((Eq.{1} ((x : #3) -> #3)) (fun (x : #3) => (#1 (#2 #0)))) #0)))))
checked 1 declarations, 1 failed, in 0.00317006s wall (2.46737e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/117_reflOccLeft"

Expected: ✋ reject · Size: 3.7 KB · Lines: 61 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 16 ms · instructions: 6.7 M · max rss memory: 21.7 MB

stderr:

loaded 2 declarations, 41 exprs (41 unique), 15 names in 0.000129223s
declaration order verified in 6.983e-06s
environment built in 1.2975e-05s; checking with 4 worker processes
FAIL reflOccLeft (line 61): arg #1 of 'reflOccLeft.mk' has a non positive occurrence of the datatypes being declared
checked 1 declarations, 1 failed, in 0.00219266s wall (1.47591e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/118_reflOccInIndex"

Expected: ✋ reject · Size: 3.9 KB · Lines: 66 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 38 ms · instructions: 6.7 M · max rss memory: 21.8 MB

stderr:

loaded 2 declarations, 45 exprs (45 unique), 16 names in 0.000150322s
declaration order verified in 1.095e-05s
environment built in 3.2831e-05s; checking with 4 worker processes
FAIL reflOccInIndex (line 66): application type mismatch in (reflOccInIndex $3)
  argument type: Nat
  expected: Sort(1)
checked 1 declarations, 1 failed, in 0.00263095s wall (2.03245e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/119_reduceCtorParamRefl.mk"

Expected: 👍 accept · Size: 4.5 KB · Lines: 88 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 18 ms · instructions: 6.8 M · max rss memory: 21.6 MB

stderr:

loaded 3 declarations, 62 exprs (62 unique), 18 names in 0.000119814s
declaration order verified in 9.036e-06s
environment built in 1.7132e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00276009s wall (1.62052e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/120_reduceCtorParamRefl2.mk"

Expected: 👍 accept · Size: 4.5 KB · Lines: 88 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 17 ms · instructions: 6.8 M · max rss memory: 21.6 MB

stderr:

loaded 3 declarations, 62 exprs (62 unique), 18 names in 0.000147957s
declaration order verified in 7.604e-06s
environment built in 1.7303e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00272814s wall (2.00647e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/121_rTreeRec"

Expected: 👍 accept · Size: 5.5 KB · Lines: 91 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 15 ms · instructions: 6.8 M · max rss memory: 21.7 MB

stderr:

loaded 3 declarations, 60 exprs (60 unique), 24 names in 0.000145402s
declaration order verified in 2.805e-06s
environment built in 1.9947e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00226532s wall (1.38685e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/122_rtreeRecReduction"

Expected: 👍 accept · Size: 10.7 KB · Lines: 191 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 17 ms · instructions: 7.4 M · max rss memory: 21.6 MB

stderr:

loaded 6 declarations, 134 exprs (134 unique), 47 names in 0.000385283s
declaration order verified in 2.805e-06s
environment built in 2.11e-05s; checking with 4 worker processes
checked 6 declarations, 0 failed, in 0.00261937s wall (1.92791e-06 core-hours over 4 workers); 14 reduction steps; peak 19 MB in one worker

Test "tutorial/123_accRecType"

Expected: 👍 accept · Size: 7.5 KB · Lines: 151 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 17 ms · instructions: 7.4 M · max rss memory: 21.6 MB

stderr:

loaded 2 declarations, 124 exprs (124 unique), 21 names in 0.000148549s
declaration order verified in 5.621e-06s
environment built in 1.592e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00364886s wall (2.31146e-06 core-hours over 4 workers); 0 reduction steps; peak 20 MB in one worker

Test "tutorial/124_accRecReduction"

Expected: 👍 accept · Size: 13.0 KB · Lines: 243 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 25 ms · instructions: 8.5 M · max rss memory: 21.7 MB

stderr:

loaded 4 declarations, 193 exprs (193 unique), 42 names in 0.000470632s
declaration order verified in 3.607e-06s
environment built in 2.09e-05s; checking with 4 worker processes
checked 4 declarations, 0 failed, in 0.0072115s wall (4.44237e-06 core-hours over 4 workers); 9 reduction steps; peak 21 MB in one worker

Test "tutorial/125_accRecNoEta"

Expected: ✋ reject · Size: 12.7 KB · Lines: 235 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 21 ms · instructions: 8.2 M · max rss memory: 21.6 MB

stderr:

loaded 4 declarations, 186 exprs (186 unique), 41 names in 0.000346479s
declaration order verified in 3.567e-06s
environment built in 2.6139e-05s; checking with 4 worker processes
FAIL accRecNoEta (line 235): declaration type mismatch for 'accRecNoEta'
  inferred: ((α : Sort(1)) -> ((r : ((a._@._internal._hyg.0 : #0) -> ((a._@._internal._hyg.0 : #1) -> Sort(0)))) -> ((a : #1) -> ((h : (((Acc.{1} #2) #1) #0)) -> ((a : Bool) -> (((Eq.{1} Bool) #0) #0))))))
  declared: ((α : Sort(1)) -> ((r : ((a._@._internal._hyg.0 : #0) -> ((a._@._internal._hyg.0 : #1) -> Sort(0)))) -> ((a : #1) -> ((h : (((Acc.{1} #2) #1) #0)) -> ((p : Bool) -> (((Eq.{1} Bool) ((((((Acc.rec.{1, 1} #4) #3) (fun (x._@.Tutorial.4017164079._hygCtx._hyg.22 : #4) => (fun (x._@.Tutorial.4017164079._hygCtx._hyg.24 : (((Acc.{1} #5) #4) #0)) => Bool))) (fun (x._@.Tutorial.4017164079._hygCtx._hyg.31 : #4) => (fun (x._@.Tutorial.4017164079._hygCtx._hyg.33 : ((y : #5) -> ((a._@._internal._hyg.0 : ((#5 #0) #1)) -> (((Acc.{1} #7) #6) #1)))) => (fun (x._@.Tutorial.4017164079._hygCtx._hyg.35 : ((y : #6) -> ((a._@._internal._hyg.0 : ((#6 #0) #2)) -> Bool))) => #3)))) #2) #1)) #0))))))
checked 3 declarations, 1 failed, in 0.00566812s wall (3.37802e-06 core-hours over 4 workers); 0 reduction steps; peak 21 MB in one worker

Test "tutorial/126_quotMkType"

Expected: 👍 accept · Size: 6.3 KB · Lines: 123 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 20 ms · instructions: 6.8 M · max rss memory: 21.5 MB

stderr:

loaded 6 declarations, 87 exprs (87 unique), 26 names in 0.000121879s
declaration order verified in 5.55e-06s
environment built in 1.2754e-05s; checking with 4 worker processes
checked 6 declarations, 0 failed, in 0.00289091s wall (1.568e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/127_quotIndType"

Expected: 👍 accept · Size: 6.3 KB · Lines: 124 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 20 ms · instructions: 6.8 M · max rss memory: 21.6 MB

stderr:

loaded 6 declarations, 88 exprs (88 unique), 26 names in 0.000203963s
declaration order verified in 2.976e-06s
environment built in 2.9826e-05s; checking with 4 worker processes
checked 6 declarations, 0 failed, in 0.00342665s wall (2.62925e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/128_quotLiftType"

Expected: 👍 accept · Size: 6.3 KB · Lines: 124 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 21 ms · instructions: 6.8 M · max rss memory: 21.6 MB

stderr:

loaded 6 declarations, 88 exprs (88 unique), 26 names in 0.000139662s
declaration order verified in 6.503e-06s
environment built in 1.6281e-05s; checking with 4 worker processes
checked 6 declarations, 0 failed, in 0.00343067s wall (2.09582e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/129_quotSoundType"

Expected: 👍 accept · Size: 7.2 KB · Lines: 141 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 21 ms · instructions: 6.9 M · max rss memory: 21.7 MB

stderr:

loaded 7 declarations, 103 exprs (103 unique), 27 names in 0.000219992s
declaration order verified in 3.848e-06s
environment built in 3.192e-05s; checking with 4 worker processes
checked 7 declarations, 0 failed, in 0.0036281s wall (2.60754e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/130_quotLiftReduction"

Expected: 👍 accept · Size: 7.8 KB · Lines: 153 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 15 ms · instructions: 7.1 M · max rss memory: 21.7 MB

stderr:

loaded 6 declarations, 116 exprs (116 unique), 27 names in 0.000105708s
declaration order verified in 4.799e-06s
environment built in 1.7503e-05s; checking with 4 worker processes
checked 6 declarations, 0 failed, in 0.003254s wall (1.86787e-06 core-hours over 4 workers); 2 reduction steps; peak 20 MB in one worker

Test "tutorial/131_quotIndReduction"

Expected: 👍 accept · Size: 7.6 KB · Lines: 151 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 16 ms · instructions: 7.1 M · max rss memory: 21.8 MB

stderr:

loaded 6 declarations, 115 exprs (115 unique), 26 names in 0.000123221s
declaration order verified in 2.094e-06s
environment built in 1.3766e-05s; checking with 4 worker processes
checked 6 declarations, 0 failed, in 0.00308289s wall (1.82496e-06 core-hours over 4 workers); 2 reduction steps; peak 20 MB in one worker

Test "tutorial/132_dup_defs"

Expected: ✋ reject · Size: 475 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 12 ms · instructions: 6.3 M · max rss memory: 21.8 MB

stderr:

loaded 2 declarations, 2 exprs (2 unique), 1 names in 9.8334e-05s
declaration order verified in 1.764e-06s
error: constant already declared: dup_defs

Test "tutorial/133_dup_ind_def"

Expected: ✋ reject · Size: 1.7 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 13 ms · instructions: 6.3 M · max rss memory: 21.9 MB

stderr:

loaded 2 declarations, 15 exprs (15 unique), 7 names in 0.000104015s
declaration order verified in 2.134e-06s
error: constant already declared: dup_ind_def

Test "tutorial/134_dup_ctor_def"

Expected: ✋ reject · Size: 1.7 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 12 ms · instructions: 6.3 M · max rss memory: 22.2 MB

stderr:

loaded 2 declarations, 15 exprs (15 unique), 7 names in 8.9949e-05s
declaration order verified in 2.415e-06s
error: constant already declared: dup_ctor_def.mk

Test "tutorial/135_dup_rec_def"

Expected: ✋ reject · Size: 1.7 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 13 ms · instructions: 6.3 M · max rss memory: 21.9 MB

stderr:

loaded 2 declarations, 15 exprs (15 unique), 7 names in 8.6662e-05s
declaration order verified in 4.628e-06s
error: constant already declared: dup_rec_def.rec

Test "tutorial/136_misnamed_rec_user"

Expected: ✋ reject · Size: 2.0 KB · Lines: 33 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 14 ms · instructions: 6.4 M · max rss memory: 21.6 MB

stderr:

loaded 2 declarations, 18 exprs (18 unique), 9 names in 0.000105017s
declaration order verified in 1.994e-06s
environment built in 1.2032e-05s; checking with 4 worker processes
FAIL misnamed_rec (line 25): recursor 'misnamed_rec.rec' missing from the export
checked 0 declarations, 1 failed, in 0.00162225s wall (1.13211e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/137_dup_rec_def2"

Expected: ✋ reject · Size: 1.7 KB · Lines: 28 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 17 ms · instructions: 6.4 M · max rss memory: 21.6 MB

stderr:

loaded 2 declarations, 15 exprs (15 unique), 8 names in 0.000123622s
declaration order verified in 2.024e-06s
environment built in 1.3446e-05s; checking with 4 worker processes
FAIL dup_rec_def2 (line 28): recursor 'dup_rec_def2.rec' missing from the export
checked 1 declarations, 1 failed, in 0.00221181s wall (1.44053e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/138_dup_ctor_rec"

Expected: ✋ reject · Size: 1.5 KB · Lines: 24 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 15 ms · instructions: 6.3 M · max rss memory: 21.9 MB

stderr:

loaded 1 declarations, 14 exprs (14 unique), 6 names in 0.000111018s
declaration order verified in 2.104e-06s
error: constant already declared: dup_ctor_rec.rec

Test "tutorial/139_DupConCon"

Expected: ✋ reject · Size: 2.2 KB · Lines: 34 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 13 ms · instructions: 6.3 M · max rss memory: 21.6 MB

stderr:

loaded 1 declarations, 21 exprs (21 unique), 9 names in 0.000271158s
declaration order verified in 4.528e-06s
error: constant already declared: dup_ind_con_con.mk

Test "tutorial/140_falseFromUnsafe"

Expected: ✋ reject · Size: 1.3 KB · Lines: 22 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 14 ms · instructions: 6.4 M · max rss memory: 21.6 MB

stderr:

loaded 3 declarations, 10 exprs (10 unique), 7 names in 0.000254527s
declaration order verified in 2.435e-06s
environment built in 2.2492e-05s; checking with 4 worker processes
FAIL falseFromUnsafe (line 22): invalid declaration, it uses unsafe declaration 'unsafeLoop'
checked 2 declarations, 1 failed, in 0.00170396s wall (1.26531e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "tutorial/141_falseFromPartial"

Expected: ✋ reject · Size: 1.3 KB · Lines: 22 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 16 ms · instructions: 6.4 M · max rss memory: 21.5 MB

stderr:

loaded 3 declarations, 10 exprs (10 unique), 7 names in 0.000292248s
declaration order verified in 4.919e-06s
environment built in 1.593e-05s; checking with 4 worker processes
FAIL partialLoop (line 20): invalid declaration, it uses unsafe declaration 'partialLoop'
checked 1 declarations, 1 failed, in 0.00201253s wall (1.41643e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker