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: 52 ms · instructions: 9.1 M · max rss memory: 21.2 MB

stderr:

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

Test "bugs/ctor-num-fields"

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

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

stderr:

loaded 25 declarations, 465 exprs (465 unique), 124 names in 0.000663312s
declaration order verified in 4.99e-06s
environment built in 2.2011e-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 9 declarations, 1 failed, in 0.00260207s wall (1.94149e-06 core-hours over 4 workers); 2 reduction steps; peak 20 MB in one worker

Test "bugs/k-rec-conv"

Expected: ✋ reject · Size: 13.0 KB · Lines: 243 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 10 declarations, 167 exprs (167 unique), 61 names in 0.000703808s
declaration order verified in 5.33e-06s
environment built in 3.3402e-05s; checking with 4 worker processes
FAIL bad (line 243): declaration type mismatch for 'bad'
  inferred: (((Eq.{1} T) t1) t1)
  declared: (((Eq.{1} T) t1) t2)
checked 9 declarations, 1 failed, in 0.00325667s wall (2.39722e-06 core-hours over 4 workers); 5 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: 18 ms · instructions: 8.2 M · max rss memory: 21.3 MB

stderr:

loaded 5 declarations, 58 exprs (58 unique), 21 names in 0.000307721s
declaration order verified in 2.335e-06s
environment built in 2.0618e-05s; checking with 4 worker processes
FAIL MyBool (line 86): recursor 'MyBool.rec' should only eliminate into Prop
checked 2 declarations, 1 failed, in 0.0020825s wall (1.20994e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 17 declarations, 318 exprs (318 unique), 95 names in 0.000678441s
declaration order verified in 6.502e-06s
environment built in 1.9417e-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.0029811s wall (2.25596e-06 core-hours over 4 workers); 28 reduction steps; peak 19 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: 18 ms · instructions: 7.9 M · max rss memory: 21.3 MB

stderr:

loaded 5 declarations, 59 exprs (59 unique), 22 names in 0.000439085s
declaration order verified in 1.894e-06s
environment built in 1.3775e-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.00193511s wall (1.15466e-06 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: 19 ms · instructions: 8.2 M · max rss memory: 21.4 MB

stderr:

loaded 6 declarations, 60 exprs (60 unique), 24 names in 0.000942631s
declaration order verified in 1.884e-06s
environment built in 1.3806e-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.00198743s wall (1.41216e-06 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: 20 ms · instructions: 8.0 M · max rss memory: 21.3 MB

stderr:

loaded 6 declarations, 67 exprs (67 unique), 30 names in 0.000385957s
declaration order verified in 2.474e-06s
environment built in 5.2016e-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.00190771s wall (1.3905e-06 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: 20 ms · instructions: 8.1 M · max rss memory: 21.5 MB

stderr:

loaded 6 declarations, 92 exprs (92 unique), 27 names in 0.00097448s
declaration order verified in 1.0079e-05s
environment built in 1.9557e-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.00188418s wall (1.08074e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

Test "bugs/nested-unused-param"

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

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

stderr:

loaded 35 declarations, 811 exprs (811 unique), 202 names in 0.000804614s
declaration order verified in 3.807e-06s
environment built in 2.1259e-05s; checking with 4 worker processes
FAIL e (line 1024): invalid projection C.0
FAIL bad (line 1050): invalid projection C.0
FAIL E (line 1012): invalid projection C.0
checked 31 declarations, 3 failed, in 0.00540135s wall (4.73705e-06 core-hours over 4 workers); 430 reduction steps; peak 21 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: 18 ms · instructions: 7.5 M · max rss memory: 21.3 MB

stderr:

loaded 2 declarations, 10 exprs (10 unique), 7 names in 0.000684782s
declaration order verified in 3.497e-06s
environment built in 1.5298e-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.00195702s wall (1.33894e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

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

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

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

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

stderr:

loaded 19 declarations, 217 exprs (217 unique), 80 names in 0.000378614s
declaration order verified in 3.417e-06s
environment built in 2.5748e-05s; checking with 4 worker processes
FAIL imaxProjBool (line 245): invalid projection ImaxProp.0
checked 16 declarations, 1 failed, in 0.00243495s wall (2.01771e-06 core-hours over 4 workers); 7 reduction steps; peak 19 MB in one worker

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

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

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

stderr:

loaded 117 declarations, 4392 exprs (4392 unique), 744 names in 0.00160621s
declaration order verified in 1.4547e-05s
environment built in 4.7338e-05s; checking with 4 worker processes
FAIL Native64ResultSort.asProp (line 4750): 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 4742): 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 104 declarations, 2 failed, in 0.00900685s wall (8.43274e-06 core-hours over 4 workers); 1666 reduction steps; peak 23 MB in one worker

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

Expected: ✋ reject · Size: 255.6 KB · Lines: 4.9 k · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 110 declarations, 4030 exprs (4030 unique), 708 names in 0.00188551s
declaration order verified in 1.6361e-05s
environment built in 4.2428e-05s; checking with 4 worker processes
FAIL PR14806Subst.observe (line 4846): type expected: (PR14806Subst.Owner PR14806Subst.witness)
checked 107 declarations, 1 failed, in 0.00962503s wall (9.44685e-06 core-hours over 4 workers); 2351 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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 5 declarations, 49 exprs (49 unique), 30 names in 0.000650468s
declaration order verified in 1.913e-06s
environment built in 1.8434e-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 0 declarations, 1 failed, in 0.0021252s wall (1.1428e-06 core-hours over 4 workers); 0 reduction steps; peak 18 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: 27 ms · instructions: 58.9 M · max rss memory: 23.2 MB

stderr:

loaded 118 declarations, 4596 exprs (4596 unique), 793 names in 0.00249052s
declaration order verified in 1.6961e-05s
environment built in 5.4281e-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 111 declarations, 1 failed, in 0.00952624s wall (8.68616e-06 core-hours over 4 workers); 2124 reduction steps; peak 23 MB in one worker

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

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

Test result: ✋ rejected · exit code 1 · wall time: 31 ms · instructions: 58.1 M · max rss memory: 23.4 MB

stderr:

loaded 127 declarations, 4203 exprs (4203 unique), 776 names in 0.00221223s
declaration order verified in 2.3704e-05s
environment built in 5.0133e-05s; checking with 4 worker processes
FAIL Issue.opaqueEndpoint (line 4788): 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 123 declarations, 1 failed, in 0.0112098s wall (1.04748e-05 core-hours over 4 workers); 2360 reduction steps; peak 23 MB in one worker

Test "cedar"

Expected: 👍 accept · Size: 790.9 MB · Lines: 14.6 M · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 21.0 s · instructions: 442.1 G · max rss memory: 978.0 MB

stderr:

loaded 133828 declarations, 13461542 exprs (13461542 unique), 985525 names in 1.54873s
declaration order verified in 0.0883237s
environment built in 0.0464061s; checking with 4 worker processes
checked 133828 declarations, 0 failed, in 19.3986s wall (0.0215362 core-hours over 4 workers); 86413667 reduction steps; peak 977 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: 18.9 s · instructions: 456.7 G · max rss memory: 617.9 MB

stderr:

loaded 26819 declarations, 9679077 exprs (9679077 unique), 337090 names in 0.761307s
declaration order verified in 0.0464964s
environment built in 0.00561891s; checking with 4 worker processes
checked 26819 declarations, 0 failed, in 18.0939s wall (0.0196966 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.0 KB · Lines: 1.2 k · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 39 declarations, 917 exprs (917 unique), 199 names in 0.000818373s
declaration order verified in 1.2473e-05s
environment built in 2.5136e-05s; checking with 4 worker processes
FAIL trans (line 1171): 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 38 declarations, 1 failed, in 0.00567659s wall (4.70047e-06 core-hours over 4 workers); 523 reduction steps; peak 22 MB in one worker

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

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

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

stderr:

loaded 40 declarations, 931 exprs (931 unique), 204 names in 0.000861563s
declaration order verified in 5.36e-06s
environment built in 2.6089e-05s; checking with 4 worker processes
checked 40 declarations, 0 failed, in 0.0057135s wall (5.05084e-06 core-hours over 4 workers); 537 reduction steps; peak 21 MB in one worker

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

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

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

stderr:

loaded 40 declarations, 938 exprs (938 unique), 204 names in 0.000679464s
declaration order verified in 1.1401e-05s
environment built in 2.5658e-05s; checking with 4 worker processes
checked 40 declarations, 0 failed, in 0.00638088s wall (5.60363e-06 core-hours over 4 workers); 674 reduction steps; peak 21 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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 6 declarations, 127 exprs (127 unique), 31 names in 0.000527832s
declaration order verified in 2.124e-06s
environment built in 1.8665e-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.00348948s wall (2.00961e-06 core-hours over 4 workers); 0 reduction steps; peak 20 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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 6 declarations, 131 exprs (131 unique), 31 names in 0.000602421s
declaration order verified in 2.405e-06s
environment built in 1.9456e-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.00332906s wall (1.97344e-06 core-hours over 4 workers); 0 reduction steps; peak 20 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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 8 declarations, 160 exprs (160 unique), 34 names in 0.000633849s
declaration order verified in 2.735e-06s
environment built in 1.7412e-05s; checking with 4 worker processes
checked 8 declarations, 0 failed, in 0.00346952s wall (1.97998e-06 core-hours over 4 workers); 0 reduction steps; peak 19 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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 7 declarations, 136 exprs (136 unique), 32 names in 0.000647284s
declaration order verified in 2.255e-06s
environment built in 1.631e-05s; checking with 4 worker processes
checked 7 declarations, 0 failed, in 0.00309618s wall (2.00264e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 6 declarations, 104 exprs (104 unique), 34 names in 0.000565682s
declaration order verified in 2.304e-06s
environment built in 1.2383e-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.00293787s wall (2.49144e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker

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

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

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

stderr:

loaded 3 declarations, 85 exprs (85 unique), 29 names in 0.000501914s
declaration order verified in 2.344e-06s
environment built in 1.4677e-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.00270783s wall (2.08246e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 4 exprs (4 unique), 4 names in 0.00038157s
declaration order verified in 1.493e-06s
environment built in 9.708e-06s; 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)
FAIL imaxRightSucc (line 21): declaration type mismatch for 'imaxRightSucc'
  inferred: Sort((imax u v+1)+1)
  declared: Sort((max u v+1)+1)
checked 0 declarations, 2 failed, in 0.0015947s wall (9.28586e-07 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: 16 ms · instructions: 7.5 M · max rss memory: 21.2 MB

stderr:

loaded 1 declarations, 5 exprs (5 unique), 4 names in 0.000358677s
declaration order verified in 1.433e-06s
environment built in 1.057e-05s; checking with 4 worker processes
FAIL EcosystemCase (line 13): let value type mismatch for 'u'
checked 0 declarations, 1 failed, in 0.00158199s wall (8.9304e-07 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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 4 declarations, 108 exprs (108 unique), 27 names in 0.000480945s
declaration order verified in 2.224e-06s
environment built in 1.3976e-05s; checking with 4 worker processes
checked 4 declarations, 0 failed, in 0.00346205s wall (2.00578e-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: 16 ms · instructions: 7.8 M · max rss memory: 21.2 MB

stderr:

loaded 4 declarations, 50 exprs (50 unique), 23 names in 0.000231331s
declaration order verified in 3.567e-06s
environment built in 9.978e-06s; 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.00168931s wall (9.96751e-07 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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 5 declarations, 92 exprs (92 unique), 31 names in 0.000457751s
declaration order verified in 2.224e-06s
environment built in 2.3013e-05s; checking with 4 worker processes
checked 5 declarations, 0 failed, in 0.00216815s wall (1.49695e-06 core-hours over 4 workers); 0 reduction steps; peak 18 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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 5 declarations, 92 exprs (92 unique), 31 names in 0.000692228s
declaration order verified in 2.424e-06s
environment built in 1.7613e-05s; checking with 4 worker processes
checked 5 declarations, 0 failed, in 0.00275576s wall (1.61967e-06 core-hours over 4 workers); 0 reduction steps; peak 18 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: 19 ms · instructions: 7.7 M · max rss memory: 21.3 MB

stderr:

loaded 1 declarations, 39 exprs (39 unique), 10 names in 0.000339342s
declaration order verified in 1.3976e-05s
environment built in 2.0228e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.0022383s wall (1.7414e-06 core-hours over 4 workers); 0 reduction steps; peak 18 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: 17 ms · instructions: 7.6 M · max rss memory: 21.3 MB

stderr:

loaded 1 declarations, 39 exprs (39 unique), 10 names in 0.000175176s
declaration order verified in 5.731e-06s
environment built in 1.0239e-05s; checking with 4 worker processes
FAIL LALProofParameterSwap (line 53): invalid return type for 'LALProofParameterSwap.mk'
checked 0 declarations, 1 failed, in 0.00194999s wall (1.03113e-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.2 KB · Lines: 1.2 k · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 41 declarations, 921 exprs (921 unique), 205 names in 0.000687489s
declaration order verified in 8.776e-06s
environment built in 3.6809e-05s; checking with 4 worker processes
checked 41 declarations, 0 failed, in 0.0066796s wall (5.95391e-06 core-hours over 4 workers); 716 reduction steps; peak 21 MB in one worker

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

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

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

stderr:

loaded 40 declarations, 903 exprs (903 unique), 201 names in 0.000985443s
declaration order verified in 1.088e-05s
environment built in 2.9044e-05s; checking with 4 worker processes
FAIL reduct (line 1160): 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 39 declarations, 1 failed, in 0.00762992s wall (6.17708e-06 core-hours over 4 workers); 557 reduction steps; peak 22 MB in one worker

Test "cslib"

Expected: 👍 accept · Size: 2.0 GB · Lines: 37.5 M · lean4export: 3.1.0 · Lean: 4.30.0 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 1.1 m · instructions: 1.2 T · max rss memory: 2.3 GB

stderr:

loaded 370939 declarations, 34998459 exprs (34998459 unique), 2155654 names in 4.53151s
declaration order verified in 0.285133s
environment built in 0.182052s; checking with 4 worker processes
checked 370939 declarations, 0 failed, in 59.0824s wall (0.0656081 core-hours over 4 workers); 182612243 reduction steps; peak 2382 MB in one worker

Test "init"

Expected: 👍 accept · Size: 309.5 MB · Lines: 6.1 M · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 9.5 s · instructions: 212.9 G · max rss memory: 374.0 MB

stderr:

loaded 53093 declarations, 5726477 exprs (5726477 unique), 278268 names in 0.562277s
declaration order verified in 0.0339655s
environment built in 0.0138079s; checking with 4 worker processes
checked 53093 declarations, 0 failed, in 8.93201s wall (0.00991444 core-hours over 4 workers); 49519537 reduction steps; peak 373 MB in one worker

Test "init-prelude"

Expected: 👍 accept · Size: 3.5 MB · Lines: 63.7 k · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 60 ms · instructions: 606.4 M · max rss memory: 29.9 MB

stderr:

loaded 1777 declarations, 54535 exprs (54535 unique), 7297 names in 0.0132059s
declaration order verified in 0.000392161s
environment built in 0.000455861s; checking with 4 worker processes
checked 1777 declarations, 0 failed, in 0.0302226s wall (3.14958e-05 core-hours over 4 workers); 33541 reduction steps; peak 27 MB in one worker

Test "mathlib"

Expected: 👍 accept · Size: 5.2 GB · Lines: 100.0 M · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 5.4 m · instructions: 5.5 T · max rss memory: 5.6 GB

stderr:

loaded 654504 declarations, 95334373 exprs (95334373 unique), 3971928 names in 14.4939s
declaration order verified in 0.875799s
environment built in 0.341208s; checking with 4 worker processes
checked 654504 declarations, 0 failed, in 308.629s wall (0.342833 core-hours over 4 workers); 687645772 reduction steps; peak 5732 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: 32 ms · instructions: 7.5 M · max rss memory: 21.3 MB

stderr:

loaded 2 declarations, 10 exprs (10 unique), 7 names in 0.000192732s
declaration order verified in 7.955e-06s
environment built in 3.178e-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.00273007s wall (1.88117e-06 core-hours over 4 workers); 0 reduction steps; peak 18 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: 18 ms · instructions: 7.4 M · max rss memory: 21.2 MB

stderr:

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

Test "other/nat-lit-add"

Expected: 👍 accept · Size: 25.7 KB · Lines: 473 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 15 declarations, 360 exprs (360 unique), 89 names in 0.00119185s
declaration order verified in 1.1621e-05s
environment built in 2.3775e-05s; checking with 4 worker processes
checked 15 declarations, 0 failed, in 0.00470443s wall (3.79337e-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.0 KB · Lines: 460 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

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

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

stderr:

loaded 14 declarations, 349 exprs (349 unique), 88 names in 0.000705974s
declaration order verified in 7.124e-06s
environment built in 2.0429e-05s; checking with 4 worker processes
FAIL natAddLitBad (line 460): 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 13 declarations, 1 failed, in 0.00382302s wall (3.15513e-06 core-hours over 4 workers); 62 reduction steps; peak 20 MB in one worker

Test "other/nat-lit-ble"

Expected: 👍 accept · Size: 28.5 KB · Lines: 515 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 16 declarations, 391 exprs (391 unique), 99 names in 0.000750688s
declaration order verified in 7.314e-06s
environment built in 3.0868e-05s; checking with 4 worker processes
checked 16 declarations, 0 failed, in 0.00456229s wall (3.58723e-06 core-hours over 4 workers); 105 reduction steps; peak 20 MB in one worker

Test "other/nat-lit-sub"

Expected: 👍 accept · Size: 29.7 KB · Lines: 556 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 19 declarations, 390 exprs (390 unique), 138 names in 0.00086381s
declaration order verified in 5.761e-06s
environment built in 1.7513e-05s; checking with 4 worker processes
checked 19 declarations, 0 failed, in 0.0037966s wall (3.29449e-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: 17 ms · instructions: 7.5 M · max rss memory: 21.3 MB

stderr:

loaded 2 declarations, 10 exprs (10 unique), 8 names in 0.000123472s
declaration order verified in 3.928e-06s
environment built in 1.4467e-05s; checking with 4 worker processes
FAIL False (line 19): constructor count mismatch in inductive block
checked 0 declarations, 1 failed, in 0.00248776s wall (1.38031e-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.29.1 · 📄 Declaration · 🔗 Source

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

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

stderr:

loaded 4 declarations, 35 exprs (35 unique), 15 names in 0.000504477s
declaration order verified in 3.377e-06s
environment built in 2.6209e-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.00258086s wall (1.65499e-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: 17 ms · instructions: 7.4 M · max rss memory: 21.3 MB

stderr:

loaded 1 declarations, 1 exprs (1 unique), 1 names in 9.6731e-05s
declaration order verified in 1.533e-06s
environment built in 1.053e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00185934s wall (1.17858e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 21 declarations, 24427 exprs (24427 unique), 4109 names in 0.00557066s
declaration order verified in 5.3921e-05s
environment built in 2.5518e-05s; checking with 4 worker processes
checked 21 declarations, 0 failed, in 1.17738s wall (0.000327766 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.29.1 · 📄 Declaration · 🔗 Source

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

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

stderr:

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

Test "perf/beta-ladder"

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

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

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

stderr:

loaded 11 declarations, 10281 exprs (10281 unique), 77 names in 0.00222404s
declaration order verified in 1.7533e-05s
environment built in 1.4077e-05s; checking with 4 worker processes
checked 11 declarations, 0 failed, in 0.333401s wall (9.39905e-05 core-hours over 4 workers); 16057 reduction steps; peak 46 MB in one worker

Test "perf/church-numerals"

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

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

Test result: 👍 accepted · exit code 0 · wall time: 30 ms · instructions: 103.0 M · max rss memory: 30.1 MB

stderr:

loaded 4 declarations, 197 exprs (197 unique), 21 names in 0.000270267s
declaration order verified in 2.024e-06s
environment built in 1.1412e-05s; checking with 4 worker processes
checked 4 declarations, 0 failed, in 0.0156412s wall (4.84011e-06 core-hours over 4 workers); 253 reduction steps; peak 30 MB in one worker

Test "perf/discarded-argument"

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

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

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

stderr:

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

Test "perf/discarded-argument-match"

Expected: 👍 accept · Size: 28.6 KB · Lines: 596 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

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

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

stderr:

loaded 15 declarations, 490 exprs (490 unique), 83 names in 0.000310783s
declaration order verified in 4.418e-06s
environment built in 1.5429e-05s; checking with 4 worker processes
checked 15 declarations, 0 failed, in 0.0232683s wall (7.96959e-06 core-hours over 4 workers); 46978 reduction steps; peak 24 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.29.1 · 📄 Declaration · 🔗 Source

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

Test result: 👍 accepted · exit code 0 · wall time: 24 ms · instructions: 30.2 M · max rss memory: 24.6 MB

stderr:

loaded 9 declarations, 1180 exprs (1180 unique), 65 names in 0.000691668s
declaration order verified in 1.6832e-05s
environment built in 2.4867e-05s; checking with 4 worker processes
checked 9 declarations, 0 failed, in 0.00887257s wall (3.66656e-06 core-hours over 4 workers); 20033 reduction steps; peak 24 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.29.1 · 📄 Declaration · 🔗 Source

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

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

stderr:

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

Test "perf/fueled-chain"

Expected: 👍 accept · Size: 476.7 KB · Lines: 9.3 k · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 137 declarations, 8205 exprs (8205 unique), 918 names in 0.0015672s
declaration order verified in 2.0669e-05s
environment built in 5.8009e-05s; checking with 4 worker processes
checked 137 declarations, 0 failed, in 0.0478614s wall (2.93934e-05 core-hours over 4 workers); 14869 reduction steps; peak 25 MB in one worker

Test "perf/grind-ring-5"

Expected: 👍 accept · Size: 9.7 MB · Lines: 199.2 k · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2185 declarations, 180991 exprs (180991 unique), 15962 names in 0.0283303s
declaration order verified in 0.000648246s
environment built in 0.000499597s; checking with 4 worker processes
checked 2185 declarations, 0 failed, in 0.445195s wall (0.000220865 core-hours over 4 workers); 2383683 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.29.1 · 📄 Declaration · 🔗 Source

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

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

stderr:

loaded 8 declarations, 128 exprs (128 unique), 32 names in 0.000360156s
declaration order verified in 2.194e-06s
environment built in 2.119e-05s; checking with 4 worker processes
checked 8 declarations, 0 failed, in 0.00281857s wall (2.09463e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "perf/irrelevance-before-evaluation"

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

slowTriv (count #n) = True.intro

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

stderr:

loaded 7 declarations, 325 exprs (325 unique), 53 names in 0.000953829s
declaration order verified in 4.298e-06s
environment built in 2.3204e-05s; checking with 4 worker processes
checked 7 declarations, 0 failed, in 0.00341334s wall (2.79532e-06 core-hours over 4 workers); 8 reduction steps; peak 18 MB in one worker

Test "perf/let-ladder"

Expected: 👍 accept · Size: 457.3 KB · Lines: 10.4 k · lean4export: 3.1.0 · Lean: 4.29.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: 185 ms · instructions: 2.2 G · max rss memory: 36.5 MB

stderr:

loaded 13 declarations, 10292 exprs (10292 unique), 84 names in 0.00453854s
declaration order verified in 1.9507e-05s
environment built in 2.0839e-05s; checking with 4 worker processes
checked 13 declarations, 0 failed, in 0.164129s wall (4.7394e-05 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.6 k · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 479 declarations, 17728 exprs (17728 unique), 3395 names in 0.00374852s
declaration order verified in 0.000121277s
environment built in 0.000118101s; checking with 4 worker processes
checked 479 declarations, 0 failed, in 0.173509s wall (5.98e-05 core-hours over 4 workers); 2804197 reduction steps; peak 29 MB in one worker

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

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

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

stderr:

loaded 479 declarations, 18849 exprs (18849 unique), 3467 names in 0.0067358s
declaration order verified in 0.000116749s
environment built in 0.000144471s; checking with 4 worker processes
checked 479 declarations, 0 failed, in 1.87851s wall (0.000535513 core-hours over 4 workers); 47639472 reduction steps; peak 45 MB in one worker

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

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

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

stderr:

loaded 263 declarations, 8858 exprs (8858 unique), 1887 names in 0.00336951s
declaration order verified in 2.631e-05s
environment built in 9.8955e-05s; checking with 4 worker processes
checked 263 declarations, 0 failed, in 7.66069s wall (0.00210662 core-hours over 4 workers); 33691152 reduction steps; peak 1364 MB in one worker

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

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

Test result: 👍 accepted · exit code 0 · wall time: 492 ms · instructions: 3.1 G · max rss memory: 128.4 MB

stderr:

loaded 263 declarations, 8868 exprs (8868 unique), 1887 names in 0.00268459s
declaration order verified in 3.1499e-05s
environment built in 7.7695e-05s; checking with 4 worker processes
checked 263 declarations, 0 failed, in 0.474075s wall (0.000139177 core-hours over 4 workers); 2520320 reduction steps; peak 128 MB in one worker

Test "perf/magma-string-n4"

Expected: 👍 accept · Size: 16.4 MB · Lines: 342.4 k · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 557 ms · instructions: 11.4 G · max rss memory: 53.2 MB

stderr:

loaded 3173 declarations, 319701 exprs (319701 unique), 19463 names in 0.0371949s
declaration order verified in 0.00113265s
environment built in 0.000495249s; checking with 4 worker processes
checked 3173 declarations, 0 failed, in 0.505196s wall (0.000533056 core-hours over 4 workers); 3333772 reduction steps; peak 52 MB in one worker

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

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

Test result: 👍 accepted · exit code 0 · wall time: 1.6 s · instructions: 20.9 G · max rss memory: 157.6 MB

stderr:

loaded 3173 declarations, 319722 exprs (319722 unique), 19463 names in 0.0480809s
declaration order verified in 0.00130701s
environment built in 0.000582413s; checking with 4 worker processes
checked 3173 declarations, 0 failed, in 1.56357s wall (0.000826958 core-hours over 4 workers); 14207475 reduction steps; peak 157 MB in one worker

Test "perf/refute-cheap-first"

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

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

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

stderr:

loaded 7 declarations, 367 exprs (367 unique), 57 names in 0.000752171s
declaration order verified in 3.947e-06s
environment built in 2.0528e-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.0117944s wall (4.46544e-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.29.1 · 📄 Declaration · 🔗 Source

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

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

stderr:

loaded 7 declarations, 367 exprs (367 unique), 57 names in 0.000311555s
declaration order verified in 2.726e-06s
environment built in 1.9487e-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.0109908s wall (4.06379e-06 core-hours over 4 workers); 6 reduction steps; peak 23 MB in one worker

Test "perf/repeated-subproblem"

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

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

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

stderr:

loaded 5 declarations, 162 exprs (162 unique), 43 names in 0.000557526s
declaration order verified in 2.264e-06s
environment built in 2.142e-05s; checking with 4 worker processes
checked 5 declarations, 0 failed, in 0.00383981s wall (2.42894e-06 core-hours over 4 workers); 132 reduction steps; peak 19 MB in one worker

Test "perf/shared-subterm"

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

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

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

stderr:

loaded 8 declarations, 1175 exprs (1175 unique), 65 names in 0.000795903s
declaration order verified in 4.899e-06s
environment built in 1.5159e-05s; checking with 4 worker processes
checked 8 declarations, 0 failed, in 0.0194502s wall (6.1452e-06 core-hours over 4 workers); 50009 reduction steps; peak 27 MB in one worker

Test "perf/shift-cascade"

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

Test result: 👍 accepted · exit code 0 · wall time: 73 ms · instructions: 529.7 M · max rss memory: 32.6 MB

stderr:

loaded 5 declarations, 4089 exprs (4089 unique), 1032 names in 0.00135441s
declaration order verified in 7.524e-06s
environment built in 1.2202e-05s; checking with 4 worker processes
checked 5 declarations, 0 failed, in 0.05552s wall (1.61716e-05 core-hours over 4 workers); 1000 reduction steps; peak 32 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.29.1 · 📄 Declaration · 🔗 Source

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

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

stderr:

loaded 5 declarations, 1107 exprs (1107 unique), 43 names in 0.000432151s
declaration order verified in 2.986e-06s
environment built in 1.5149e-05s; checking with 4 worker processes
checked 5 declarations, 0 failed, in 0.00233907s wall (1.71119e-06 core-hours over 4 workers); 17 reduction steps; peak 18 MB in one worker

Test "std"

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

Test result: 👍 accepted · exit code 0 · wall time: 18.2 s · instructions: 351.1 G · max rss memory: 670.4 MB

stderr:

loaded 90778 declarations, 9396483 exprs (9396483 unique), 535158 names in 1.52589s
declaration order verified in 0.0636212s
environment built in 0.0309619s; checking with 4 worker processes
checked 90778 declarations, 0 failed, in 16.6258s wall (0.0184496 core-hours over 4 workers); 69377453 reduction steps; peak 670 MB in one worker

Test "tutorial/001_basicDef"

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

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

stderr:

loaded 1 declarations, 2 exprs (2 unique), 1 names in 0.000249759s
declaration order verified in 1.994e-06s
environment built in 1.1732e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00214464s wall (1.48017e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 1 declarations, 2 exprs (2 unique), 1 names in 9.3916e-05s
declaration order verified in 1.823e-06s
environment built in 1.3946e-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.00188177s wall (1.30937e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/003_arrowType"

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

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

stderr:

loaded 1 declarations, 3 exprs (3 unique), 6 names in 0.00012787s
declaration order verified in 2.154e-06s
environment built in 1.3486e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00183071s wall (1.2949e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 1 declarations, 3 exprs (3 unique), 2 names in 0.00010671s
declaration order verified in 1.743e-06s
environment built in 1.1151e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00245381s wall (1.55449e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 1 declarations, 6 exprs (6 unique), 8 names in 0.000111509s
declaration order verified in 1.613e-06s
environment built in 1.6661e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00262545s wall (1.49512e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 13 exprs (13 unique), 10 names in 0.000114846s
declaration order verified in 4.639e-06s
environment built in 1.4898e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00348624s wall (1.69192e-06 core-hours over 4 workers); 1 reduction steps; peak 17 MB in one worker

Test "tutorial/007_betaReduction2"

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

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

stderr:

loaded 2 declarations, 14 exprs (14 unique), 10 names in 0.000114805s
declaration order verified in 5.189e-06s
environment built in 1.3786e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00252167s wall (1.68069e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 13 exprs (13 unique), 6 names in 0.000115246s
declaration order verified in 3.126e-06s
environment built in 2.146e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00212375s wall (1.45197e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 14 exprs (14 unique), 6 names in 0.000121248s
declaration order verified in 1.833e-06s
environment built in 1.563e-05s; checking with 4 worker processes
FAIL forallSortBad (line 26): type expected: $1
checked 1 declarations, 1 failed, in 0.00250111s wall (1.50722e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 8 exprs (8 unique), 9 names in 0.000106459s
declaration order verified in 1.723e-06s
environment built in 1.1392e-05s; checking with 4 worker processes
FAIL nonTypeType (line 21): type expected: constType
checked 1 declarations, 1 failed, in 0.00262293s wall (1.55315e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

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

Test "tutorial/012_nonPropThm"

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

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

stderr:

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

Test "tutorial/013_thmProof"

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

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

stderr:

loaded 2 declarations, 14 exprs (14 unique), 9 names in 0.000115687s
declaration order verified in 5.049e-06s
environment built in 1.8084e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00256794s wall (1.45881e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

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

Test "tutorial/015_levelComp1"

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

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

stderr:

loaded 1 declarations, 2 exprs (2 unique), 1 names in 7.3628e-05s
declaration order verified in 1.603e-06s
environment built in 1.1331e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00160983s wall (1.07369e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 1 declarations, 2 exprs (2 unique), 1 names in 0.00010658s
declaration order verified in 1.793e-06s
environment built in 1.1521e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00191242s wall (1.37082e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 1 declarations, 2 exprs (2 unique), 1 names in 0.000136767s
declaration order verified in 1.803e-06s
environment built in 1.075e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00195285s wall (1.32858e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 13 exprs (13 unique), 11 names in 0.00012814s
declaration order verified in 5.21e-06s
environment built in 1.3846e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00259969s wall (1.51729e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 1 declarations, 2 exprs (2 unique), 2 names in 6.8038e-05s
declaration order verified in 1.754e-06s
environment built in 1.066e-05s; checking with 4 worker processes
FAIL tut06_bad01 (line 8): duplicate universe level parameter 'u'
checked 0 declarations, 1 failed, in 0.00167427s wall (9.78252e-07 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/020_levelComp4"

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

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

stderr:

loaded 1 declarations, 2 exprs (2 unique), 2 names in 0.00012231s
declaration order verified in 2.084e-06s
environment built in 1.2534e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00196152s wall (1.37696e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 1 declarations, 2 exprs (2 unique), 2 names in 0.000129313s
declaration order verified in 1.623e-06s
environment built in 1.6932e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00170422s wall (1.20583e-06 core-hours over 4 workers); 0 reduction steps; peak 17 MB in one worker

Test "tutorial/022_imax1"

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

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

stderr:

loaded 1 declarations, 6 exprs (6 unique), 7 names in 0.000132719s
declaration order verified in 7.774e-06s
environment built in 1.9217e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00225728s wall (1.50839e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 1 declarations, 6 exprs (6 unique), 7 names in 0.000112371s
declaration order verified in 5.13e-06s
environment built in 1.3055e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00228427s wall (1.63062e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 1 declarations, 2 exprs (2 unique), 3 names in 0.000129614s
declaration order verified in 2.796e-06s
environment built in 1.8214e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00178771s wall (1.15712e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 1 declarations, 2 exprs (2 unique), 4 names in 0.000125616s
declaration order verified in 1.883e-06s
environment built in 1.4888e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00155017s wall (1.07496e-06 core-hours over 4 workers); 0 reduction steps; peak 17 MB in one worker

Test "tutorial/026_levelMaxIdem"

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

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

stderr:

loaded 1 declarations, 2 exprs (2 unique), 2 names in 0.000124754s
declaration order verified in 3.937e-06s
environment built in 1.4227e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.0020433s wall (1.39674e-06 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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 1 declarations, 2 exprs (2 unique), 3 names in 0.00010658s
declaration order verified in 1.724e-06s
environment built in 1.6511e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.0016747s wall (1.1697e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 1 declarations, 7 exprs (7 unique), 3 names in 0.000130345s
declaration order verified in 1.773e-06s
environment built in 1.3094e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.0019251s wall (1.40533e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 1 declarations, 15 exprs (15 unique), 9 names in 0.000116869s
declaration order verified in 3.947e-06s
environment built in 1.1201e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00227038s wall (1.68653e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 7 declarations, 41 exprs (41 unique), 20 names in 0.000121138s
declaration order verified in 3.637e-06s
environment built in 1.056e-05s; checking with 4 worker processes
checked 7 declarations, 0 failed, in 0.00187224s wall (1.40662e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 8 declarations, 55 exprs (55 unique), 22 names in 0.000120817s
declaration order verified in 3.446e-06s
environment built in 1.5278e-05s; checking with 4 worker processes
checked 8 declarations, 0 failed, in 0.0025116s wall (1.82324e-06 core-hours over 4 workers); 23 reduction steps; peak 18 MB in one worker

Test "tutorial/032_peano3"

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

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

stderr:

loaded 10 declarations, 59 exprs (59 unique), 24 names in 0.000137568s
declaration order verified in 3.576e-06s
environment built in 1.4628e-05s; checking with 4 worker processes
checked 10 declarations, 0 failed, in 0.00211213s wall (1.37982e-06 core-hours over 4 workers); 37 reduction steps; peak 18 MB in one worker

Test "tutorial/033_letType"

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

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

stderr:

loaded 1 declarations, 4 exprs (4 unique), 2 names in 0.000107712s
declaration order verified in 1.964e-06s
environment built in 1.3295e-05s; checking with 4 worker processes
checked 1 declarations, 0 failed, in 0.00203959s wall (1.41041e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 3 declarations, 11 exprs (11 unique), 10 names in 0.000115607s
declaration order verified in 2.034e-06s
environment built in 2.0018e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.002674s wall (1.53608e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 5 exprs (5 unique), 3 names in 0.000108794s
declaration order verified in 3.887e-06s
environment built in 1.046e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.0027109s wall (1.85783e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 9 exprs (9 unique), 6 names in 0.000133982s
declaration order verified in 1.843e-06s
environment built in 1.4658e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00273162s wall (1.61427e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 22 exprs (22 unique), 10 names in 0.000146786s
declaration order verified in 1.633e-06s
environment built in 1.5068e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00208593s wall (1.48165e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 3 declarations, 43 exprs (43 unique), 16 names in 0.000143849s
declaration order verified in 4.108e-06s
environment built in 1.4407e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00299171s wall (1.78487e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 41 exprs (41 unique), 12 names in 0.000109005s
declaration order verified in 4.448e-06s
environment built in 1.0921e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00196105s wall (1.5313e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/040_prodType"

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

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

stderr:

loaded 2 declarations, 47 exprs (47 unique), 19 names in 0.000141275s
declaration order verified in 3.526e-06s
environment built in 1.5108e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00211096s wall (1.58952e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/041_pprodType"

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

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

stderr:

loaded 2 declarations, 47 exprs (47 unique), 19 names in 0.00012791s
declaration order verified in 3.607e-06s
environment built in 1.4387e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.0021246s wall (1.66887e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/042_pUnitType"

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

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

stderr:

loaded 2 declarations, 16 exprs (16 unique), 9 names in 0.000107171s
declaration order verified in 4.629e-06s
environment built in 1.3776e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00209154s wall (1.27768e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 42 exprs (42 unique), 15 names in 0.000136826s
declaration order verified in 3.516e-06s
environment built in 2.2382e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00231167s wall (1.86474e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/044_natDef"

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

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

stderr:

loaded 2 declarations, 36 exprs (36 unique), 20 names in 0.000384712s
declaration order verified in 3.407e-06s
environment built in 1.6642e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00189765s wall (1.45264e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 4 declarations, 248 exprs (248 unique), 39 names in 0.000729709s
declaration order verified in 2.885e-06s
environment built in 2.1771e-05s; checking with 4 worker processes
checked 4 declarations, 0 failed, in 0.00480069s wall (2.28138e-06 core-hours over 4 workers); 0 reduction steps; peak 20 MB in one worker

Test "tutorial/046_inductBadNonSort"

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

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

stderr:

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

Test "tutorial/047_inductBadNonSort2"

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

Test result: ✋ rejected · exit code 1 · wall time: 58 ms · instructions: 7.5 M · max rss memory: 21.3 MB

stderr:

loaded 2 declarations, 2 exprs (2 unique), 2 names in 0.000120195s
declaration order verified in 2.134e-06s
environment built in 1.6701e-05s; checking with 4 worker processes
FAIL inductBadNonSort2 (line 8): type expected: aType
checked 1 declarations, 1 failed, in 0.00198111s wall (1.36347e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

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

Test "tutorial/049_inductTooFewParams"

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

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

stderr:

loaded 1 declarations, 2 exprs (2 unique), 2 names in 0.000188364s
declaration order verified in 3.927e-06s
environment built in 2.5428e-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.00291568s wall (2.10332e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 7 exprs (7 unique), 5 names in 0.000152607s
declaration order verified in 2.896e-06s
environment built in 1.2713e-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.00180181s wall (1.31652e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 1 declarations, 11 exprs (11 unique), 5 names in 0.000143729s
declaration order verified in 1.773e-06s
environment built in 1.1822e-05s; checking with 4 worker processes
FAIL inductWrongCtorResParams (line 19): invalid return type for 'inductWrongCtorResParams.mk'
checked 0 declarations, 1 failed, in 0.00175119s wall (1.27045e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

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

Test "tutorial/053_inductInIndex"

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

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

stderr:

loaded 2 declarations, 6 exprs (6 unique), 5 names in 0.000132569s
declaration order verified in 2.114e-06s
environment built in 1.9757e-05s; checking with 4 worker processes
FAIL inductInIndex (line 14): invalid return type for 'inductInIndex.mk'
checked 1 declarations, 1 failed, in 0.00236647s wall (1.68978e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 1 declarations, 5 exprs (5 unique), 4 names in 0.000103454s
declaration order verified in 2.394e-06s
environment built in 1.4818e-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.00206227s wall (1.46085e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 3 declarations, 54 exprs (54 unique), 18 names in 0.000153147s
declaration order verified in 3.577e-06s
environment built in 2.0849e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00178126s wall (1.3714e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/056_reduceCtorType.mk"

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

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

stderr:

loaded 2 declarations, 13 exprs (13 unique), 7 names in 0.000140404s
declaration order verified in 2.665e-06s
environment built in 1.7182e-05s; checking with 4 worker processes
FAIL reduceCtorType (line 26): invalid return type for 'reduceCtorType.mk'
checked 1 declarations, 1 failed, in 0.00209946s wall (1.58946e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 3 declarations, 14 exprs (14 unique), 12 names in 0.000145473s
declaration order verified in 1.853e-06s
environment built in 1.9887e-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.00267378s wall (1.41581e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 20 exprs (20 unique), 8 names in 0.000144461s
declaration order verified in 2.154e-06s
environment built in 1.589e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00193507s wall (1.45413e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 21 exprs (21 unique), 9 names in 0.000125145s
declaration order verified in 1.783e-06s
environment built in 1.1332e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00205991s wall (1.50632e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 21 exprs (21 unique), 10 names in 0.000149431s
declaration order verified in 1.904e-06s
environment built in 2.2562e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00241742s wall (1.46758e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 1 declarations, 4 exprs (4 unique), 4 names in 0.000188844s
declaration order verified in 1.944e-06s
environment built in 1.0911e-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.00160353s wall (1.12808e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 10 exprs (10 unique), 6 names in 0.000119614s
declaration order verified in 2.235e-06s
environment built in 1.8484e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.0022408s wall (1.62861e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 32 exprs (32 unique), 16 names in 0.000140794s
declaration order verified in 3.597e-06s
environment built in 2.5548e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.0026353s wall (1.64527e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 3 declarations, 50 exprs (50 unique), 22 names in 0.000130685s
declaration order verified in 3.988e-06s
environment built in 1.1752e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00189823s wall (1.43158e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 42 exprs (42 unique), 12 names in 0.000115927s
declaration order verified in 3.567e-06s
environment built in 2.0037e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00205643s wall (1.68928e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/066_prodRec"

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

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

stderr:

loaded 2 declarations, 49 exprs (49 unique), 20 names in 0.000146745s
declaration order verified in 4.167e-06s
environment built in 1.5669e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00247121s wall (1.72811e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 48 exprs (48 unique), 20 names in 0.000142998s
declaration order verified in 4.738e-06s
environment built in 1.584e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00212896s wall (1.31988e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 18 exprs (18 unique), 15 names in 9.8575e-05s
declaration order verified in 4.298e-06s
environment built in 1.1552e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00210765s wall (1.11342e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 43 exprs (43 unique), 15 names in 0.000108914s
declaration order verified in 6.372e-06s
environment built in 1.3996e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00161123s wall (1.22753e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/070_nRec"

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

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

stderr:

loaded 2 declarations, 36 exprs (36 unique), 20 names in 0.000104687s
declaration order verified in 3.256e-06s
environment built in 1.6832e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00162448s wall (1.05619e-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.29.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 67 ms · instructions: 10.4 M · max rss memory: 21.1 MB

stderr:

loaded 4 declarations, 254 exprs (254 unique), 40 names in 0.000277591s
declaration order verified in 2.575e-06s
environment built in 1.3174e-05s; checking with 4 worker processes
checked 4 declarations, 0 failed, in 0.00468243s wall (2.25602e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 22 exprs (22 unique), 9 names in 8.9909e-05s
declaration order verified in 4.408e-06s
environment built in 1.3626e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00189164s wall (1.12815e-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.29.1 · 📄 Declaration · 🔗 Source

inductive BogusRecursor : Type where
  | mk : BogusRecursor

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

stderr:

loaded 3 declarations, 12 exprs (12 unique), 9 names in 8.0992e-05s
declaration order verified in 1.953e-06s
environment built in 1.7744e-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.00168776s wall (1.18727e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/074_existsRec"

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

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

stderr:

loaded 2 declarations, 45 exprs (45 unique), 17 names in 8.8707e-05s
declaration order verified in 3.858e-06s
environment built in 1.1842e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00194439s wall (1.40022e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 5 declarations, 95 exprs (95 unique), 34 names in 0.000143189s
declaration order verified in 2.014e-06s
environment built in 1.587e-05s; checking with 4 worker processes
checked 5 declarations, 0 failed, in 0.00172106s wall (1.3727e-06 core-hours over 4 workers); 5 reduction steps; peak 18 MB in one worker

Test "tutorial/076_sortElimPropRec"

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

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

stderr:

loaded 3 declarations, 69 exprs (69 unique), 22 names in 0.000101129s
declaration order verified in 1.974e-06s
environment built in 1.1312e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00192041s wall (1.37187e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 4 declarations, 83 exprs (83 unique), 24 names in 0.00010139s
declaration order verified in 1.893e-06s
environment built in 1.3986e-05s; checking with 4 worker processes
checked 4 declarations, 0 failed, in 0.00207215s wall (1.48113e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 4 declarations, 133 exprs (133 unique), 58 names in 0.000284524s
declaration order verified in 2.565e-06s
environment built in 1.2263e-05s; checking with 4 worker processes
checked 4 declarations, 0 failed, in 0.00272343s wall (1.84773e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 3 declarations, 127 exprs (127 unique), 67 names in 0.000198101s
declaration order verified in 2.325e-06s
environment built in 1.1261e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.003248s wall (1.84572e-06 core-hours over 4 workers); 6 reduction steps; peak 19 MB in one worker

Test "tutorial/080_nRecReduction"

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

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

stderr:

loaded 6 declarations, 170 exprs (170 unique), 58 names in 0.000262903s
declaration order verified in 2.224e-06s
environment built in 1.4016e-05s; checking with 4 worker processes
checked 6 declarations, 0 failed, in 0.00298094s wall (2.06227e-06 core-hours over 4 workers); 43 reduction steps; peak 19 MB in one worker

Test "tutorial/081_listRecReduction"

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

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

stderr:

loaded 7 declarations, 256 exprs (256 unique), 67 names in 0.000238828s
declaration order verified in 2.324e-06s
environment built in 1.4276e-05s; checking with 4 worker processes
checked 7 declarations, 0 failed, in 0.00438007s wall (2.65008e-06 core-hours over 4 workers); 44 reduction steps; peak 20 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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 7 declarations, 878 exprs (878 unique), 116 names in 0.000404949s
declaration order verified in 7.845e-06s
environment built in 1.6591e-05s; checking with 4 worker processes
checked 7 declarations, 0 failed, in 0.00728475s wall (4.45176e-06 core-hours over 4 workers); 46 reduction steps; peak 21 MB in one worker

Test "tutorial/083_And.right"

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

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

stderr:

loaded 3 declarations, 55 exprs (55 unique), 14 names in 0.000154881s
declaration order verified in 1.1612e-05s
environment built in 2.2081e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00325549s wall (2.20736e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 3 declarations, 57 exprs (57 unique), 16 names in 0.000128181s
declaration order verified in 6.983e-06s
environment built in 1.3545e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00240805s wall (1.54403e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/085_PProd.snd"

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

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

stderr:

loaded 3 declarations, 57 exprs (57 unique), 16 names in 0.000144982s
declaration order verified in 3.998e-06s
environment built in 2.2072e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00194653s wall (1.52209e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/086_PSigma.snd"

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

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

stderr:

loaded 3 declarations, 65 exprs (65 unique), 21 names in 0.000112581s
declaration order verified in 1.733e-06s
environment built in 2.0278e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00239306s wall (1.56444e-06 core-hours over 4 workers); 1 reduction steps; peak 18 MB in one worker

Test "tutorial/087_projOutOfRange"

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

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

stderr:

loaded 2 declarations, 48 exprs (48 unique), 15 names in 0.000110047s
declaration order verified in 4.889e-06s
environment built in 1.3996e-05s; checking with 4 worker processes
FAIL projOutOfRange (line 67): invalid projection And.2
checked 1 declarations, 1 failed, in 0.00212775s wall (1.64603e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

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

Test "tutorial/089_projProp1"

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

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

stderr:

loaded 4 declarations, 103 exprs (103 unique), 31 names in 0.000427523s
declaration order verified in 3.125e-06s
environment built in 1.6701e-05s; checking with 4 worker processes
checked 4 declarations, 0 failed, in 0.00247654s wall (1.67691e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/090_projProp2"

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

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

stderr:

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

Test "tutorial/091_projProp3"

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

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

stderr:

loaded 4 declarations, 103 exprs (103 unique), 31 names in 0.000365806s
declaration order verified in 2.555e-06s
environment built in 3.716e-05s; checking with 4 worker processes
checked 4 declarations, 0 failed, in 0.00257641s wall (1.71566e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/092_projProp4"

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

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

stderr:

loaded 4 declarations, 103 exprs (103 unique), 31 names in 0.000224291s
declaration order verified in 2.324e-06s
environment built in 1.3956e-05s; checking with 4 worker processes
FAIL projProp4 (line 143): invalid projection PropStructure.3
checked 3 declarations, 1 failed, in 0.00239263s wall (1.50927e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 4 declarations, 108 exprs (108 unique), 31 names in 0.000393999s
declaration order verified in 2.896e-06s
environment built in 2.114e-05s; checking with 4 worker processes
FAIL projProp5 (line 148): invalid projection PropStructure.3
checked 3 declarations, 1 failed, in 0.00259811s wall (1.92821e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 4 declarations, 103 exprs (103 unique), 31 names in 0.000372679s
declaration order verified in 3.256e-06s
environment built in 1.8174e-05s; checking with 4 worker processes
FAIL projProp6 (line 143): invalid projection PropStructure.5
checked 3 declarations, 1 failed, in 0.00273133s wall (1.83571e-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.29.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 30 ms · instructions: 8.1 M · max rss memory: 21.3 MB

stderr:

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

Test "tutorial/096_projIndexData"

Expected: ✋ reject · Size: 6.8 KB · Lines: 111 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 4 declarations, 72 exprs (72 unique), 32 names in 0.000146495s
declaration order verified in 2.495e-06s
environment built in 2.5919e-05s; checking with 4 worker processes
FAIL projIndexData (line 111): invalid projection PropStructure.0
checked 3 declarations, 1 failed, in 0.00191556s wall (1.46699e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/097_projIndexData2"

Expected: ✋ reject · Size: 6.8 KB · Lines: 111 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 4 declarations, 72 exprs (72 unique), 32 names in 0.000158898s
declaration order verified in 3.987e-06s
environment built in 2.2762e-05s; checking with 4 worker processes
FAIL projIndexData2 (line 111): invalid projection PropStructure.1
checked 3 declarations, 1 failed, in 0.00236834s wall (1.53953e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/098_projRed"

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

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

stderr:

loaded 6 declarations, 131 exprs (131 unique), 32 names in 0.000322104s
declaration order verified in 4.529e-06s
environment built in 1.7813e-05s; checking with 4 worker processes
checked 6 declarations, 0 failed, in 0.00282381s wall (2.06796e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 3 declarations, 83 exprs (83 unique), 31 names in 0.000125155s
declaration order verified in 3.977e-06s
environment built in 1.7684e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00249793s wall (1.65278e-06 core-hours over 4 workers); 4 reduction steps; peak 18 MB in one worker

Test "tutorial/100_ruleKbad"

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

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

stderr:

loaded 3 declarations, 83 exprs (83 unique), 31 names in 0.000130495s
declaration order verified in 1.843e-06s
environment built in 1.1061e-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.00269578s wall (1.63778e-06 core-hours over 4 workers); 0 reduction steps; peak 20 MB in one worker

Test "tutorial/101_ruleKAcc"

Expected: ✋ reject · Size: 12.8 KB · Lines: 238 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 4 declarations, 189 exprs (189 unique), 41 names in 0.00028248s
declaration order verified in 2.334e-06s
environment built in 1.7813e-05s; checking with 4 worker processes
FAIL ruleKAcc (line 238): 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)) -> (((fun (x._@.Tutorial.4255978773._hygCtx._hyg.22 : #8) => (fun (x._@.Tutorial.4255978773._hygCtx._hyg.24 : (((Acc.{u} #9) #8) #0)) => Bool)) #1) ((#2 #1) #0))))) => #3)))) #2) #1)) #0))))))
checked 3 declarations, 1 failed, in 0.00433879s wall (2.7528e-06 core-hours over 4 workers); 0 reduction steps; peak 20 MB in one worker

Test "tutorial/102_aNatLit"

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

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

stderr:

loaded 2 declarations, 37 exprs (37 unique), 12 names in 0.000161843s
declaration order verified in 4.729e-06s
environment built in 2.4777e-05s; checking with 4 worker processes
checked 2 declarations, 0 failed, in 0.00285571s wall (2.43491e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 3 declarations, 84 exprs (84 unique), 23 names in 0.000124955s
declaration order verified in 2.124e-06s
environment built in 1.9607e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00275189s wall (2.14927e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 3 declarations, 66 exprs (66 unique), 28 names in 0.000108002s
declaration order verified in 7.233e-06s
environment built in 1.5609e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00238668s wall (1.57398e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/105_proofIrrelevanceBad"

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

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

stderr:

loaded 3 declarations, 67 exprs (67 unique), 19 names in 0.000125326s
declaration order verified in 2.705e-06s
environment built in 1.7633e-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.00250828s wall (1.62053e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 4 declarations, 74 exprs (74 unique), 29 names in 0.000118022s
declaration order verified in 2.224e-06s
environment built in 1.1511e-05s; checking with 4 worker processes
checked 4 declarations, 0 failed, in 0.00275351s wall (1.77149e-06 core-hours over 4 workers); 10 reduction steps; peak 18 MB in one worker

Test "tutorial/107_proofIrrelevanceUnderBinder"

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

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

stderr:

loaded 7 declarations, 17 exprs (17 unique), 13 names in 0.000116348s
declaration order verified in 1.904e-06s
environment built in 1.7583e-05s; checking with 4 worker processes
checked 7 declarations, 0 failed, in 0.00215183s wall (1.3293e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 5 declarations, 77 exprs (77 unique), 30 names in 0.000161022s
declaration order verified in 1.085e-05s
environment built in 2.2131e-05s; checking with 4 worker processes
checked 5 declarations, 0 failed, in 0.00265788s wall (1.75953e-06 core-hours over 4 workers); 4 reduction steps; peak 18 MB in one worker

Test "tutorial/109_unitEta2"

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

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

stderr:

loaded 4 declarations, 73 exprs (73 unique), 29 names in 0.000141625s
declaration order verified in 2.094e-06s
environment built in 1.8935e-05s; checking with 4 worker processes
checked 4 declarations, 0 failed, in 0.00198967s wall (1.5703e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/110_unitEta3"

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

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

stderr:

loaded 4 declarations, 75 exprs (75 unique), 29 names in 0.000160501s
declaration order verified in 3.286e-06s
environment built in 2.0779e-05s; checking with 4 worker processes
checked 4 declarations, 0 failed, in 0.00204749s wall (1.6786e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/111_indexedUnitEta"

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

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

stderr:

loaded 4 declarations, 86 exprs (86 unique), 27 names in 0.000135223s
declaration order verified in 2.265e-06s
environment built in 1.7163e-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.00265678s wall (2.04416e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 7 declarations, 173 exprs (173 unique), 43 names in 0.000965912s
declaration order verified in 4.899e-06s
environment built in 2.6169e-05s; checking with 4 worker processes
checked 7 declarations, 0 failed, in 0.00325447s wall (2.45624e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 5 declarations, 99 exprs (99 unique), 30 names in 0.000293922s
declaration order verified in 3.146e-06s
environment built in 1.8554e-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.0026401s wall (1.71445e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 3 declarations, 71 exprs (71 unique), 26 names in 0.000118583s
declaration order verified in 1.954e-06s
environment built in 1.6381e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00267775s wall (1.70662e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/115_funEtaDep"

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

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

stderr:

loaded 3 declarations, 73 exprs (73 unique), 26 names in 0.000117361s
declaration order verified in 2.435e-06s
environment built in 1.2122e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00285903s wall (1.78461e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/116_funEtaBad"

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

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

stderr:

loaded 2 declarations, 64 exprs (64 unique), 27 names in 0.00011178s
declaration order verified in 3.807e-06s
environment built in 2.8895e-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.00224155s wall (1.71358e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 41 exprs (41 unique), 15 names in 0.00011196s
declaration order verified in 4.118e-06s
environment built in 1.2142e-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.00264778s wall (1.79665e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 45 exprs (45 unique), 16 names in 9.566e-05s
declaration order verified in 3.777e-06s
environment built in 1.9106e-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.00196592s wall (1.20211e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 3 declarations, 62 exprs (62 unique), 18 names in 9.4618e-05s
declaration order verified in 3.687e-06s
environment built in 1.4116e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00252552s wall (1.5524e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 3 declarations, 62 exprs (62 unique), 18 names in 0.000120176s
declaration order verified in 4.779e-06s
environment built in 1.4968e-05s; checking with 4 worker processes
checked 3 declarations, 0 failed, in 0.00239431s wall (1.92735e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

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

Test "tutorial/122_rtreeRecReduction"

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

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

stderr:

loaded 6 declarations, 136 exprs (136 unique), 47 names in 0.000229742s
declaration order verified in 2.575e-06s
environment built in 1.2754e-05s; checking with 4 worker processes
checked 6 declarations, 0 failed, in 0.00295229s wall (1.73901e-06 core-hours over 4 workers); 13 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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

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

Test "tutorial/124_accRecReduction"

Expected: 👍 accept · Size: 13.4 KB · Lines: 252 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 4 declarations, 202 exprs (202 unique), 42 names in 0.000329127s
declaration order verified in 5.481e-06s
environment built in 2.0719e-05s; checking with 4 worker processes
checked 4 declarations, 0 failed, in 0.0045801s wall (2.9894e-06 core-hours over 4 workers); 7 reduction steps; peak 20 MB in one worker

Test "tutorial/125_accRecNoEta"

Expected: ✋ reject · Size: 13.0 KB · Lines: 244 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 4 declarations, 195 exprs (195 unique), 41 names in 0.000290525s
declaration order verified in 2.295e-06s
environment built in 2.0088e-05s; checking with 4 worker processes
FAIL accRecNoEta (line 244): 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)) -> (((fun (x._@.Tutorial.4017164079._hygCtx._hyg.22 : #8) => (fun (x._@.Tutorial.4017164079._hygCtx._hyg.24 : (((Acc.{1} #9) #8) #0)) => Bool)) #1) ((#2 #1) #0))))) => #3)))) #2) #1)) #0))))))
checked 3 declarations, 1 failed, in 0.00450191s wall (2.84929e-06 core-hours over 4 workers); 0 reduction steps; peak 20 MB in one worker

Test "tutorial/126_quotMkType"

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

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

stderr:

loaded 6 declarations, 87 exprs (87 unique), 26 names in 0.000121698s
declaration order verified in 2.685e-06s
environment built in 1.3555e-05s; checking with 4 worker processes
checked 6 declarations, 0 failed, in 0.00279985s wall (1.89881e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/127_quotIndType"

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

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

stderr:

loaded 6 declarations, 88 exprs (88 unique), 26 names in 0.000103294s
declaration order verified in 4.869e-06s
environment built in 1.559e-05s; checking with 4 worker processes
checked 6 declarations, 0 failed, in 0.00266038s wall (1.51673e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/128_quotLiftType"

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

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

stderr:

loaded 6 declarations, 88 exprs (88 unique), 26 names in 0.000132038s
declaration order verified in 2.244e-06s
environment built in 1.581e-05s; checking with 4 worker processes
checked 6 declarations, 0 failed, in 0.0023149s wall (1.98148e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/129_quotSoundType"

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

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

stderr:

loaded 7 declarations, 103 exprs (103 unique), 27 names in 0.000128201s
declaration order verified in 2.264e-06s
environment built in 2.153e-05s; checking with 4 worker processes
checked 7 declarations, 0 failed, in 0.00263849s wall (1.82966e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker

Test "tutorial/130_quotLiftReduction"

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

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

stderr:

loaded 6 declarations, 116 exprs (116 unique), 27 names in 0.000254398s
declaration order verified in 2.264e-06s
environment built in 1.4818e-05s; checking with 4 worker processes
checked 6 declarations, 0 failed, in 0.00343259s wall (1.99276e-06 core-hours over 4 workers); 2 reduction steps; peak 19 MB in one worker

Test "tutorial/131_quotIndReduction"

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

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

stderr:

loaded 6 declarations, 115 exprs (115 unique), 26 names in 0.000140092s
declaration order verified in 2.896e-06s
environment built in 1.6742e-05s; checking with 4 worker processes
checked 6 declarations, 0 failed, in 0.0034246s wall (2.16852e-06 core-hours over 4 workers); 2 reduction steps; peak 19 MB in one worker

Test "tutorial/132_dup_defs"

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

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

stderr:

loaded 2 declarations, 2 exprs (2 unique), 1 names in 8.1113e-05s
declaration order verified in 4.589e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 15 exprs (15 unique), 7 names in 0.000123191s
declaration order verified in 2.815e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 15 exprs (15 unique), 7 names in 0.000109035s
declaration order verified in 1.993e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 15 exprs (15 unique), 7 names in 0.000105979s
declaration order verified in 1.753e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 18 exprs (18 unique), 9 names in 9.6271e-05s
declaration order verified in 1.843e-06s
environment built in 1.4207e-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.00237283s wall (1.37315e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 2 declarations, 15 exprs (15 unique), 8 names in 0.000102923s
declaration order verified in 1.854e-06s
environment built in 1.6541e-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.00175152s wall (1.15322e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 1 declarations, 14 exprs (14 unique), 6 names in 0.000116038s
declaration order verified in 2.415e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 1 declarations, 21 exprs (21 unique), 9 names in 0.000113493s
declaration order verified in 1.683e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

loaded 3 declarations, 10 exprs (10 unique), 7 names in 8.1803e-05s
declaration order verified in 1.984e-06s
environment built in 1.4287e-05s; checking with 4 worker processes
FAIL falseFromUnsafe (line 22): invalid declaration, it uses unsafe declaration 'unsafeLoop'
checked 2 declarations, 1 failed, in 0.00210595s wall (1.35046e-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.29.1 · 📄 Declaration · 🔗 Source

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

stderr:

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