Lean Kernel Arena / lean4lean

Checker "lean4lean"

Version: - · 📄 Declaration · 🔗 Source

Lean4Lean is an implementation of the Lean 4 kernel written in (mostly) pure Lean 4. It is derived directly from the C++ kernel implementation, and as such likely shares some implementation bugs with it (it's not really an independent implementation), although it also benefits from the same algorithmic performance improvements existing in the C++ Lean kernel.

The project also houses some metatheory regarding the Lean system, in the same general direction as the MetaCoq project.

The lean4lean checker checks that primitive definitions from the prelude are as expected. For that reason, it is tied to a specific Lean version. The arena uses a wrapper script to switch to the appropriate version for the tests we have here.

Completeness (rightfully accepted tests)

90/90

Soundness (rightfully rejected tests)

40/40

Declined tests

6

Test Expected Result ⏱️ 🧠
bogus1 ✋ 🚫 27 ms 13.0 MB
cedar 👍 👍 4.2 m (+49%) 1.2 GB (+1%)
constlevels ✋ 🚫 26 ms 13.0 MB
cslib 👍 👍 9.2 m (+92%) 2.1 GB (-2%)
grind-ring-5 👍 🚫 26 ms 13.0 MB
init 👍 🚫 26 ms 13.0 MB
init-prelude 👍 🚫 26 ms 13.0 MB
mathlib 👍 👍 1.9 h (+188%) 11.9 GB (+31%)
mlir 👍 👍 7.0 s (+25%) 136.4 MB
std 👍 🚫 26 ms 13.0 MB
tutorial/001_basicDef 👍 👍 65 ms 88.6 MB
tutorial/002_badDef ✋ ✋ 101 ms 94.6 MB
tutorial/003_arrowType 👍 👍 65 ms 88.6 MB
tutorial/004_dependentType 👍 👍 65 ms 88.6 MB
tutorial/005_constType 👍 👍 65 ms 88.8 MB
tutorial/006_betaReduction 👍 👍 65 ms 88.9 MB
tutorial/007_betaReduction2 👍 👍 65 ms 88.9 MB
tutorial/008_forallSortWhnf 👍 👍 65 ms 88.8 MB
tutorial/009_forallSortBad ✋ ✋ 66 ms 89.9 MB
tutorial/010_nonTypeType ✋ ✋ 65 ms 89.6 MB
tutorial/011_nonPropThm ✋ ✋ 65 ms 89.1 MB
tutorial/012_levelComp1 👍 👍 65 ms 88.8 MB
tutorial/013_levelComp2 👍 👍 65 ms 88.8 MB
tutorial/014_levelComp3 👍 👍 65 ms 88.8 MB
tutorial/015_levelParams 👍 👍 65 ms 88.8 MB
tutorial/016_tut06_bad01 ✋ ✋ 65 ms 88.4 MB
tutorial/017_levelComp4 👍 👍 65 ms 88.8 MB
tutorial/018_levelComp5 👍 👍 65 ms 88.8 MB
tutorial/019_imax1 👍 👍 65 ms 88.8 MB
tutorial/020_imax2 👍 👍 65 ms 88.8 MB
tutorial/021_inferVar 👍 👍 65 ms 88.7 MB
tutorial/022_defEqLambda 👍 👍 65 ms 88.8 MB
tutorial/023_peano1 👍 👍 65 ms 89.0 MB
tutorial/024_peano2 👍 👍 65 ms 89.0 MB
tutorial/025_peano3 👍 👍 66 ms 89.0 MB
tutorial/026_letType 👍 👍 65 ms 88.8 MB
tutorial/027_letTypeDep 👍 👍 65 ms 88.9 MB
tutorial/028_letRed 👍 👍 65 ms 88.9 MB
tutorial/029_empty 👍 👍 65 ms 89.4 MB
tutorial/030_boolType 👍 👍 65 ms 89.5 MB
tutorial/031_twoBool 👍 👍 65 ms 89.6 MB
tutorial/032_andType 👍 👍 65 ms 89.5 MB
tutorial/033_prodType 👍 👍 65 ms 89.6 MB
tutorial/034_pprodType 👍 👍 65 ms 89.6 MB
tutorial/035_pUnitType 👍 👍 65 ms 89.5 MB
tutorial/036_eqType 👍 👍 65 ms 89.5 MB
tutorial/037_natDef 👍 👍 65 ms 89.6 MB
tutorial/038_rbTreeDef 👍 👍 67 ms 89.6 MB
tutorial/039_inductBadNonSort ✋ ✋ 65 ms 90.0 MB
tutorial/040_inductBadNonSort2 ✋ ✋ 65 ms 89.9 MB
tutorial/041_inductLevelParam ✋ ✋ 65 ms 88.6 MB
tutorial/042_inductTooFewParams ✋ ✋ 65 ms 88.6 MB
tutorial/043_inductWrongCtorParams ✋ ✋ 65 ms 89.4 MB
tutorial/044_inductWrongCtorResParams ✋ ✋ 65 ms 89.2 MB
tutorial/045_inductWrongCtorResLevel ✋ ✋ 65 ms 89.3 MB
tutorial/046_inductInIndex ✋ ✋ 65 ms 89.4 MB
tutorial/047_indNeg ✋ ✋ 65 ms 89.3 MB
tutorial/048_reduceCtorParam.mk 👍 👍 65 ms 89.6 MB
tutorial/049_reduceCtorType.mk ✋ ✋ 65 ms 89.4 MB
tutorial/050_indNegReducible ✋ ✋ 65 ms 89.5 MB
tutorial/051_predWithTypeField 👍 👍 65 ms 89.5 MB
tutorial/052_typeWithTypeField 👍 👍 65 ms 89.5 MB
tutorial/053_typeWithTypeFieldPoly 👍 👍 65 ms 89.5 MB
tutorial/054_typeWithTooHighTypeField.mk ✋ ✋ 65 ms 89.3 MB
tutorial/055_emptyRec 👍 👍 65 ms 89.4 MB
tutorial/056_boolRec 👍 👍 65 ms 89.5 MB
tutorial/057_twoBoolRec 👍 👍 65 ms 89.6 MB
tutorial/058_andRec 👍 👍 65 ms 89.5 MB
tutorial/059_prodRec 👍 👍 65 ms 89.5 MB
tutorial/060_pprodRec 👍 👍 65 ms 89.5 MB
tutorial/061_punitRec 👍 👍 65 ms 89.4 MB
tutorial/062_eqRec 👍 👍 65 ms 89.5 MB
tutorial/063_nRec 👍 👍 65 ms 89.5 MB
tutorial/064_rbTreeRef 👍 👍 67 ms 89.6 MB
tutorial/065_boolPropRec 👍 👍 65 ms 89.4 MB
tutorial/066_existsRec 👍 👍 65 ms 89.5 MB
tutorial/067_sortElimPropRec 👍 👍 65 ms 89.6 MB
tutorial/068_sortElimProp2Rec 👍 👍 66 ms 89.6 MB
tutorial/069_boolRecEqns 👍 👍 66 ms 89.6 MB
tutorial/070_prodRecEqns 👍 👍 66 ms 89.6 MB
tutorial/071_nRecReduction 👍 👍 66 ms 89.8 MB
tutorial/072_listRecReduction 👍 👍 67 ms 89.8 MB
tutorial/073_RBTree.id_spec 👍 👍 71 ms 89.8 MB
tutorial/074_And.right 👍 👍 65 ms 89.5 MB
tutorial/075_Prod.snd 👍 👍 65 ms 89.6 MB
tutorial/076_PProd.snd 👍 👍 65 ms 89.6 MB
tutorial/077_PSigma.snd 👍 👍 65 ms 89.6 MB
tutorial/078_projOutOfRange ✋ ✋ 66 ms 90.5 MB
tutorial/079_projNotStruct ✋ ✋ 66 ms 90.4 MB
tutorial/080_projProp1 👍 👍 66 ms 89.6 MB
tutorial/081_projProp2 ✋ ✋ 66 ms 90.5 MB
tutorial/082_projProp3 👍 👍 66 ms 89.6 MB
tutorial/083_projProp4 ✋ ✋ 66 ms 90.5 MB
tutorial/084_projProp5 ✋ ✋ 66 ms 90.5 MB
tutorial/085_projProp6 ✋ ✋ 66 ms 90.5 MB
tutorial/086_projDataIndexRec 👍 👍 66 ms 89.6 MB
tutorial/087_projIndexData ✋ ✋ 66 ms 90.5 MB
tutorial/088_projIndexData2 ✋ ✋ 66 ms 90.5 MB
tutorial/089_projRed 👍 👍 66 ms 89.6 MB
tutorial/090_ruleK 👍 👍 66 ms 89.6 MB
tutorial/091_ruleKbad ✋ ✋ 102 ms 95.5 MB
tutorial/092_ruleKAcc ✋ ✋ 104 ms 95.5 MB
tutorial/093_aNatLit 👍 👍 65 ms 89.6 MB
tutorial/094_natLitEq 👍 👍 66 ms 89.6 MB
tutorial/095_proofIrrelevance 👍 👍 65 ms 89.6 MB
tutorial/096_unitEta1 👍 👍 66 ms 89.6 MB
tutorial/097_unitEta2 👍 👍 66 ms 89.6 MB
tutorial/098_unitEta3 👍 👍 66 ms 89.6 MB
tutorial/099_structEta 👍 👍 66 ms 89.6 MB
tutorial/100_funEta 👍 👍 65 ms 89.8 MB
tutorial/101_funEtaDep 👍 👍 66 ms 89.6 MB
tutorial/102_funEtaBad ✋ ✋ 102 ms 95.5 MB
tutorial/103_etaRuleK ✋ ✋ 100 ms 95.5 MB
tutorial/104_etaCtor ✋ ✋ 101 ms 95.5 MB
tutorial/105_reflOccLeft ✋ ✋ 65 ms 89.4 MB
tutorial/106_reflOccInIndex ✋ ✋ 66 ms 90.5 MB
tutorial/107_reduceCtorParamRefl.mk 👍 👍 65 ms 89.6 MB
tutorial/108_reduceCtorParamRefl2.mk 👍 👍 65 ms 89.6 MB
tutorial/109_rTreeRec 👍 👍 65 ms 89.6 MB
tutorial/110_rtreeRecReduction 👍 👍 66 ms 89.8 MB
tutorial/111_accRecType 👍 👍 66 ms 89.6 MB
tutorial/112_accRecReduction 👍 👍 66 ms 89.6 MB
tutorial/113_accRecNoEta ✋ ✋ 104 ms 95.5 MB
tutorial/114_quotMkType 👍 👍 65 ms 89.5 MB
tutorial/115_quotIndType 👍 👍 66 ms 89.5 MB
tutorial/116_quotLiftType 👍 👍 65 ms 89.5 MB
tutorial/117_quotSoundType 👍 👍 66 ms 89.5 MB
tutorial/118_quotLiftReduction 👍 👍 66 ms 89.6 MB
tutorial/119_quotIndReduction 👍 👍 66 ms 89.6 MB
tutorial/120_dup_defs ✋ ✋ 65 ms 88.3 MB
tutorial/121_dup_ind_def ✋ ✋ 65 ms 88.4 MB
tutorial/122_dup_ctor_def ✋ ✋ 65 ms 88.4 MB
tutorial/123_dup_rec_def ✋ ✋ 65 ms 88.4 MB
tutorial/124_dup_rec_def2 ✋ ✋ 65 ms 89.5 MB
tutorial/125_dup_ctor_rec ✋ ✋ 65 ms 88.4 MB
tutorial/126_DupConCon ✋ ✋ 65 ms 88.4 MB

Detailed results

Test "bogus1"

Expected: ✋ reject · Size: 11.4 KB · Lines: 198 · lean4export: 3.1.0 · Lean: 4.29.0-rc1 · 📄 Declaration · 🔗 Source

A clearly bogus proof. Also serves as an example for how to write simple cases.

Test result: 🚫 declined · exit code 2 · wall time: 67 ms · instructions: 161.2 M · max rss memory: 13.0 MB

stderr:
Error: Unknown toolchain: 4.29.0-rc1
Known toolchains: 4.26.0, 4.27.0-nightly-2025-12-01, 4.27.0-rc1, 4.28.0-nightly-2026-01-19, 4.28.0-nightly-2026-01-20

Test "cedar"

Expected: 👍 accept · Size: 728.6 MB · Lines: 13.4 M · lean4export: 3.1.0 · Lean: 4.26.0 · 📄 Declaration · 🔗 Source

Lean formalization of, and proofs about, Cedar.

Auto-generated documentation is available at https://cedar-policy.github.io/cedar-spec/docs/.

This test case exports the whole Cedar module and as such contains even unused parts Init and Batteries.

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

stdout:
[anonymous]:thmDecl _private.Cedar.Thm.SymCC.Data.LT.0.Cedar.Thm.Op.mkName.neq: lean4lean took 1108
checked 114854 declarations

Test "constlevels"

Expected: ✋ reject · Size: 15.3 KB · Lines: 283 · lean4export: 3.1.0 · Lean: 4.29.0-rc2 · 📄 Declaration

Regression test for undefined behavior in lazy_delta_reduction_step in the official kernel

In the function lazy_delta_reduction_step, the official kernel expects unfold_definition to always succeed. However, if the constant has an incorrect number of level parameters, it actually fails, which leads to memory corruption in lazy_delta_reduction_step.

This test is to check that the official kernel and also other kernels that closely follow the logic of the official kernel correctly handle this unfolding failure.

The issue in the official kernel was originally reported as https://github.com/leanprover/lean4/issues/10577.

Test result: 🚫 declined · exit code 2 · wall time: 33 ms · instructions: 155.9 M · max rss memory: 13.0 MB

stderr:
Error: Unknown toolchain: 4.29.0-rc2
Known toolchains: 4.26.0, 4.27.0-nightly-2025-12-01, 4.27.0-rc1, 4.28.0-nightly-2026-01-19, 4.28.0-nightly-2026-01-20

Test "cslib"

Expected: 👍 accept · Size: 1.2 GB · Lines: 22.8 M · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

The Lean Computer Science Library (CSLib).

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

stdout:
checked 253619 declarations

Test "grind-ring-5"

Expected: 👍 accept · Size: 9.7 MB · Lines: 199.5 k · lean4export: 3.1.0 · Lean: 4.29.0-rc1 · 📄 Declaration · 🔗 Source

A grind tactic test from the Lean 4 test suite.

This produces a theorem with a rather large proof term that needs fast reduction.

Test result: 🚫 declined · exit code 2 · wall time: 45 ms · instructions: 155.9 M · max rss memory: 13.0 MB

stderr:
Error: Unknown toolchain: 4.29.0-rc1
Known toolchains: 4.26.0, 4.27.0-nightly-2025-12-01, 4.27.0-rc1, 4.28.0-nightly-2026-01-19, 4.28.0-nightly-2026-01-20

Test "init"

Expected: 👍 accept · Size: 307.1 MB · Lines: 6.0 M · lean4export: 3.1.0 · Lean: 4.29.0-rc1 · 📄 Declaration · 🔗 Source

The Init module export from Lean 4 core.

This test contains the fundamental building blocks of Lean 4, including:

  • Basic data types (Nat, List, Array, String, etc.)
  • Core tactics and syntax
  • Foundational mathematical structures
  • Essential metaprogramming infrastructure

This is one of the smallest meaningful test cases, making it ideal for initial checker validation and debugging.

Test result: 🚫 declined · exit code 2 · wall time: 35 ms · instructions: 156.0 M · max rss memory: 13.0 MB

stderr:
Error: Unknown toolchain: 4.29.0-rc1
Known toolchains: 4.26.0, 4.27.0-nightly-2025-12-01, 4.27.0-rc1, 4.28.0-nightly-2026-01-19, 4.28.0-nightly-2026-01-20

Test "init-prelude"

Expected: 👍 accept · Size: 3.5 MB · Lines: 63.5 k · lean4export: 3.1.0 · Lean: 4.29.0-rc1 · 📄 Declaration · 🔗 Source

The Init.Prelude module export.

Test result: 🚫 declined · exit code 2 · wall time: 35 ms · instructions: 155.9 M · max rss memory: 13.0 MB

stderr:
Error: Unknown toolchain: 4.29.0-rc1
Known toolchains: 4.26.0, 4.27.0-nightly-2025-12-01, 4.27.0-rc1, 4.28.0-nightly-2026-01-19, 4.28.0-nightly-2026-01-20

Test "mathlib"

Expected: 👍 accept · Size: 4.9 GB · Lines: 92.5 M · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

The complete Mathlib library export.

This test contains all the mathematical definitions, theorems, and proofs from Mathlib, representing the largest and most comprehensive test case in the Lean kernel arena.

This test is based on a commit that includes https://github.com/leanprover-community/mathlib4/pull/33794 to include the performance fix therein.

Test result: 👍 accepted · exit code 0 · wall time: 2.5 h · instructions: 41.1 T · max rss memory: 11.9 GB

stdout:
[anonymous]:thmDecl RingCat.instCreatesLimitSemiRingCatForget₂._proof_16: lean4lean took 1119
[anonymous]:thmDecl CommRingCat.instCreatesLimitRingCatForget₂._proof_5: lean4lean took 1159
[anonymous]:thmDecl ModuleCat.monoidalCategory._proof_4: lean4lean took 10517
[anonymous]:thmDecl KaehlerDifferential.mvPolynomialEquiv._proof_1: lean4lean took 2247
[anonymous]:thmDecl KaehlerDifferential.mvPolynomialEquiv._proof_2: lean4lean took 2119
[anonymous]:thmDecl Ideal.powQuotSuccInclusion_apply_coe: lean4lean took 1630
[anonymous]:thmDecl Ideal.powQuotSuccInclusion_injective: lean4lean took 6990
[anonymous]:thmDecl AlgebraicGeometry.AffineSpace.homOfVector_appTop_coord: lean4lean took 10609
[anonymous]:thmDecl AlgebraicGeometry.AffineSpace.isoOfIsAffine._proof_4: lean4lean took 2088
[anonymous]:thmDecl AlgebraicGeometry.AffineSpace.isoOfIsAffine._proof_1: lean4lean took 2079
[anonymous]:thmDecl IsAlgebraic.adjoin_of_forall_isAlgebraic: lean4lean took 1096
[anonymous]:thmDecl AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord: lean4lean took 5295
[anonymous]:thmDecl AlgebraicGeometry.AffineSpace.map_SpecMap: lean4lean took 5595
[anonymous]:thmDecl SheafOfModules.instHasColimitsOfShapeOfPresheafOfModulesValRingCat: lean4lean took 1742
[anonymous]:thmDecl Submodule.pow_induction_on_left': lean4lean took 1950
[anonymous]:thmDecl CliffordAlgebra.GradedAlgebra.lift_ι_eq: lean4lean took 4213
[anonymous]:defnDecl PresheafOfModules.pushforwardComp: lean4lean took 1092
[anonymous]:thmDecl Algebra.TensorProduct.opAlgEquiv._proof_3: lean4lean took 1633
[anonymous]:defnDecl SheafOfModules.pushforwardComp: lean4lean took 1309
[anonymous]:thmDecl CommAlgCat.instBraidedCategory._proof_4: lean4lean took 10510
[anonymous]:thmDecl PresheafOfModules.freeObj._proof_2: lean4lean took 72549
[anonymous]:thmDecl InfiniteGalois.algEquivToLimit._proof_3: lean4lean took 1033
[anonymous]:thmDecl Algebra.Generators.CotangentSpace.compEquiv_symm_inr: lean4lean took 2327
[anonymous]:thmDecl Algebra.Generators.CotangentSpace.fst_compEquiv: lean4lean took 1854
[anonymous]:thmDecl BialgCat.MonoidalCategory.inducingFunctorData._proof_4: lean4lean took 1009
[anonymous]:thmDecl BialgCat.MonoidalCategory.inducingFunctorData._proof_5: lean4lean took 2890
[anonymous]:thmDecl BialgCat.MonoidalCategory.inducingFunctorData._proof_11: lean4lean took 1239
[anonymous]:thmDecl IntermediateField.adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable: lean4lean took 2175
[anonymous]:thmDecl TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_symm: lean4lean took 1130
[anonymous]:thmDecl commBialgCatEquivComonCommAlgCat._proof_13: lean4lean took 1254
[anonymous]:defnDecl _private.Mathlib.AlgebraicGeometry.RationalMap.0.AlgebraicGeometry.Scheme.PartialMap.equivalence_rel.match_1_1: lean4lean took 7268
[anonymous]:thmDecl AlgebraicGeometry.Scheme.PartialMap.equivalence_rel: lean4lean took 6337
[anonymous]:thmDecl CategoryTheory.Abelian.Ext.preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply: lean4lean took 1072
[anonymous]:thmDecl CategoryTheory.Abelian.Ext.covariant_sequence_exact₁': lean4lean took 2283
[anonymous]:thmDecl AlgebraicGeometry.compactSpace_of_universallyClosed: lean4lean took 2061
[anonymous]:thmDecl GradedTensorProduct.tmul_coe_mul_coe_tmul: lean4lean took 4667
[anonymous]:thmDecl CommAlgCat.instBraidedCategory._proof_3: lean4lean took 8236
[anonymous]:thmDecl CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply: lean4lean took 1123
[anonymous]:thmDecl CategoryTheory.Abelian.Ext.contravariant_sequence_exact₁': lean4lean took 2322
[anonymous]:thmDecl groupHomology.mapShortComplexH1_comp: lean4lean took 5614
[anonymous]:thmDecl AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop: lean4lean took 4714
[anonymous]:thmDecl AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop: lean4lean took 2415
[anonymous]:thmDecl Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual: lean4lean took 1073
[anonymous]:thmDecl eventually_norm_mfderivWithin_symm_extChartAt_comp_lt: lean4lean took 1008
[anonymous]:thmDecl ContinuousMultilinearMap.hasStrictFDerivAt_compContinuousLinearMap: lean4lean took 1105
[anonymous]:thmDecl Algebra.TensorProduct.tensorTensorTensorComm_symm: lean4lean took 1330
[anonymous]:defnDecl AlgebraicGeometry.Scheme.RationalMap.compHom.match_1: lean4lean took 8057
[anonymous]:thmDecl AlgebraicGeometry.Scheme.RationalMap.compHom._proof_1: lean4lean took 235356
[anonymous]:thmDecl AlgebraicGeometry.Scheme.RationalMap.equivFunctionField._proof_4: lean4lean took 259576
[anonymous]:thmDecl AlgebraicGeometry.Scheme.RationalMap.equivFunctionField._proof_5: lean4lean took 279281
[anonymous]:defnDecl ContinuousCohomology.MultiInd.d: lean4lean took 1027
[anonymous]:thmDecl ContinuousCohomology.MultiInd.d_comp_d: lean4lean took 13810
[anonymous]:thmDecl IntermediateField.Lifts.union_isExtendible: lean4lean took 2709
[anonymous]:thmDecl DoubleQuot.quotQuotEquivComm_symmₐ: lean4lean took 24600
[anonymous]:thmDecl GradedTensorProduct.comm._proof_4: lean4lean took 1617
[anonymous]:thmDecl CategoryTheory.Abelian.Ext.contravariant_sequence_exact₃': lean4lean took 2587
[anonymous]:thmDecl PresheafOfModules.DifferentialsConstruction.relativeDifferentials'._proof_2: lean4lean took 27836
[anonymous]:thmDecl Field.Emb.Cardinal.instIsSeparableSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet: lean4lean took 2915
[anonymous]:thmDecl AddCommGrpCat.Colimits.quotUliftToQuot_ι: lean4lean took 1327
[anonymous]:thmDecl Field.Emb.Cardinal.succEquiv_coherence: lean4lean took 1477
[anonymous]:thmDecl AlgebraicGeometry.Scheme.PartialMap.restrict_equiv: lean4lean took 24535
[anonymous]:thmDecl AlgebraicGeometry.Scheme.RationalMap.isOver_iff: lean4lean took 205327
[anonymous]:thmDecl fromModuleCatToModuleCatLinearEquivtoModuleCatObj._proof_5: lean4lean took 2270
[anonymous]:defnDecl fromModuleCatToModuleCatLinearEquivtoModuleCatObj: lean4lean took 1111
[anonymous]:thmDecl fromModuleCatToModuleCatLinearEquivtoModuleCatObj.eq_1: lean4lean took 1120
[anonymous]:defnDecl _private.Mathlib.AlgebraicGeometry.RationalMap.0.AlgebraicGeometry.Scheme.PartialMap.equiv_iff_of_isSeparated_of_le.match_1_1: lean4lean took 7196
[anonymous]:thmDecl AlgebraicGeometry.Scheme.PartialMap.equiv_iff_of_isSeparated_of_le: lean4lean took 3875
[anonymous]:thmDecl AlgebraicGeometry.Scheme.RationalMap.toPartialMap._proof_6: lean4lean took 2074
[anonymous]:thmDecl AlgebraicGeometry.Scheme.RationalMap.equivFunctionField._proof_8: lean4lean took 243495
[anonymous]:thmDecl AlgebraicGeometry.Scheme.PartialMap.equiv_of_fromSpecStalkOfMem_eq: lean4lean took 2560
[anonymous]:thmDecl AlgebraicGeometry.Scheme.RationalMap.equivFunctionField._proof_9: lean4lean took 237880
[anonymous]:thmDecl AlgCat.forget₂Ring_preservesLimitsOfSize: lean4lean took 1205
[anonymous]:thmDecl CategoryTheory.Abelian.Ext.covariant_sequence_exact₃': lean4lean took 2714
[anonymous]:thmDecl AlgebraicGeometry.Scheme.PartialMap.equiv_iff_of_domain_eq_of_isSeparated: lean4lean took 2154
[anonymous]:thmDecl IntermediateField.sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable: lean4lean took 1113
[anonymous]:thmDecl AlgebraicGeometry.Scheme.RationalMap.equivFunctionField._proof_6: lean4lean took 235139
[anonymous]:thmDecl Algebra.FormallyEtale.of_isSeparable: lean4lean took 6923
[anonymous]:thmDecl CoalgCat.MonoidalCategoryAux.comul_tensorObj_tensorObj_left: lean4lean took 6750
[anonymous]:thmDecl PadicInt.coe_adicCompletionIntegersEquiv_symm_apply: lean4lean took 45245
[anonymous]:thmDecl _private.Batteries.Data.List.Scan.0.List.drop_scanr._proof_1_2: lean4lean took 1075
[anonymous]:thmDecl Algebra.Generators.H1Cotangent.δAux_ofComp: lean4lean took 2239
[anonymous]:thmDecl Algebra.TensorProduct.toLinearEquiv_tensorTensorTensorComm: lean4lean took 2705
[anonymous]:thmDecl _private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle.0.Real.Angle.abs_toReal_add_eq_two_pi_sub_abs_toReal_add_abs_toReal_aux._proof_1_2: lean4lean took 1896
[anonymous]:thmDecl PadicInt.coe_adicCompletionIntegersEquiv_apply: lean4lean took 41767
[anonymous]:thmDecl TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_eq: lean4lean took 2427
[anonymous]:thmDecl Algebra.IsInvariant.exists_smul_of_under_eq_of_profinite: lean4lean took 1362
[anonymous]:thmDecl exteriorPower.pairingDual_apply_apply_eq_one: lean4lean took 1012
[anonymous]:thmDecl LinearMap.lTensor_tensor: lean4lean took 10309
[anonymous]:thmDecl Algebra.Generators.H1Cotangent.exact_map_δ': lean4lean took 1088
[anonymous]:thmDecl Algebra.TensorProduct.algEquivIncludeRange_toAlgHom: lean4lean took 1341
[anonymous]:defnDecl SheafOfModules.sheafificationCompPullback: lean4lean took 1470
[anonymous]:thmDecl CoalgCat.MonoidalCategoryAux.comul_tensorObj_tensorObj_right: lean4lean took 4995
[anonymous]:thmDecl GradedTensorProduct.comm_coe_tmul_coe: lean4lean took 1305
[anonymous]:thmDecl AlgebraicGeometry.Scheme.PartialMap.restrict_restrict_hom: lean4lean took 19812
[anonymous]:thmDecl TensorProduct.map_convMul_map: lean4lean took 2555
[anonymous]:thmDecl AlgebraicGeometry.Scheme.PartialMap.exists_restrict_isOver: lean4lean took 6458
[anonymous]:thmDecl CoalgCat.MonoidalCategoryAux.comul_tensorObj: lean4lean took 2452
[anonymous]:thmDecl exteriorPower.pairingDual_apply_apply_eq_one_zero: lean4lean took 1026
[anonymous]:thmDecl Polynomial.taylorLinearEquiv_symm: lean4lean took 320616
[anonymous]:thmDecl Algebra.Generators.CotangentSpace.compEquiv.eq_1: lean4lean took 1069
[anonymous]:thmDecl TensorProduct.AlgebraTensorModule.assoc_eq: lean4lean took 1039
[anonymous]:thmDecl DoubleQuot.quotQuotEquivComm_symm: lean4lean took 21915
[anonymous]:thmDecl LinearMap.rTensor_tensor: lean4lean took 1400
checked 614144 declarations

Test "mlir"

Expected: 👍 accept · Size: 28.8 MB · Lines: 576.3 k · lean4export: 3.1.0 · Lean: 4.27.0-nightly-2025-12-01 · 📄 Declaration · 🔗 Source

The main theorems from lean-mlir.

Test result: 👍 accepted · exit code 0 · wall time: 5.3 s · instructions: 41.8 G · max rss memory: 136.4 MB

stdout:
checked 4497 declarations

Test "std"

Expected: 👍 accept · Size: 522.7 MB · Lines: 10.0 M · lean4export: 3.1.0 · Lean: 4.29.0-rc1 · 📄 Declaration · 🔗 Source

The complete Std library export from Lean 4.

This test contains the standard library extensions beyond core Lean 4, including:

  • Enhanced data structures (HashMap, RBTree, etc.)
  • Additional mathematical operations
  • Extended list and array operations
  • Utility functions and theorems

This represents a medium-sized test case, larger than core modules but smaller than Mathlib, making it useful for performance testing.

Test result: 🚫 declined · exit code 2 · wall time: 34 ms · instructions: 155.8 M · max rss memory: 13.0 MB

stderr:
Error: Unknown toolchain: 4.29.0-rc1
Known toolchains: 4.26.0, 4.27.0-nightly-2025-12-01, 4.27.0-rc1, 4.28.0-nightly-2026-01-19, 4.28.0-nightly-2026-01-20

Test "tutorial/001_basicDef"

Expected: 👍 accept · Size: 371 B · Lines: 6 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

Basic definition

Test result: 👍 accepted · exit code 0 · wall time: 98 ms · instructions: 389.3 M · max rss memory: 88.6 MB

stdout:
checked 1 declarations

Test "tutorial/002_badDef"

Expected: ✋ reject · Size: 369 B · Lines: 6 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

Mismatched types

Test result: ✋ rejected · exit code 1 · wall time: 125 ms · instructions: 607.4 M · max rss memory: 94.6 MB

stderr:
PANIC at _private.Lean.Environment.0.Lean.EnvExtension.getStateImpl Lean.Environment:1341:4: invalid environment extension has been accessed
backtrace:
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(+0x93104ee) [0x55555e8644ee]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lean_panic_fn+0x1c) [0x55555e86497c]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l___private_Lean_Environment_0__Lean_EnvExtension_getStateUnsafe___redArg+0x8f7) [0x55555735fb17]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_ppExprWithInfos+0x17a) [0x555558ebb33a]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_ofExpr___lam__1+0x4e) [0x55555793066e]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lean_apply_2+0x9e9) [0x55555e872149]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x12b) [0x5555579323cb]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6e9) [0x555557932989]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x362) [0x555557932602]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6e9) [0x555557932989]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6d8) [0x555557932978]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6d8) [0x555557932978]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_toString+0x15) [0x555557933535]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_throwKernelException___redArg+0x7fb) [0x555556fd0c0b]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replayConstant___lam__0+0x25) [0x555556fd38e5]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replayConstant+0x3332) [0x555556fd82e2]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_Std_DTreeMap_Internal_Impl_forInStep___at___00replayConstants_spec__0+0x135) [0x555556fdbbb5]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replay+0x168) [0x555556fdf7e8]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(_lean_main+0x360) [0x555556fea2b0]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(+0x1a75c92) [0x555556fc9c92]
/nix/store/xx7cm72qy2c0643cm1ipngd87aqwkcdp-glibc-2.40-66/lib/libc.so.6(+0x2a4d8) [0x7ffff7c2a4d8]
/nix/store/xx7cm72qy2c0643cm1ipngd87aqwkcdp-glibc-2.40-66/lib/libc.so.6(__libc_start_main+0x8b) [0x7ffff7c2a59b]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(_start+0x25) [0x555556fcad95]
PANIC at _private.Lean.Environment.0.Lean.EnvExtension.getStateImpl Lean.Environment:1341:4: invalid environment extension has been accessed
backtrace:
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(+0x93104ee) [0x55555e8644ee]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lean_panic_fn+0x1c) [0x55555e86497c]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l___private_Lean_Environment_0__Lean_EnvExtension_getStateUnsafe___redArg+0x8f7) [0x55555735fb17]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_ppExprWithInfos+0x17a) [0x555558ebb33a]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_ofExpr___lam__1+0x4e) [0x55555793066e]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lean_apply_2+0x9e9) [0x55555e872149]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x12b) [0x5555579323cb]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6e9) [0x555557932989]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x362) [0x555557932602]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6e9) [0x555557932989]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_toString+0x15) [0x555557933535]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_throwKernelException___redArg+0x7fb) [0x555556fd0c0b]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replayConstant___lam__0+0x25) [0x555556fd38e5]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replayConstant+0x3332) [0x555556fd82e2]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_Std_DTreeMap_Internal_Impl_forInStep___at___00replayConstants_spec__0+0x135) [0x555556fdbbb5]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replay+0x168) [0x555556fdf7e8]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(_lean_main+0x360) [0x555556fea2b0]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(+0x1a75c92) [0x555556fc9c92]
/nix/store/xx7cm72qy2c0643cm1ipngd87aqwkcdp-glibc-2.40-66/lib/libc.so.6(+0x2a4d8) [0x7ffff7c2a4d8]
/nix/store/xx7cm72qy2c0643cm1ipngd87aqwkcdp-glibc-2.40-66/lib/libc.so.6(__libc_start_main+0x8b) [0x7ffff7c2a59b]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(_start+0x25) [0x555556fcad95]
uncaught exception: at badDef: (kernel) declaration type mismatch, 'badDef' has type
  [Error pretty printing expression: (`Inhabited.default` for `IO.Error`). Falling back to raw printer.]
  Type.{1}
but it is expected to have type
  [Error pretty printing expression: (`Inhabited.default` for `IO.Error`). Falling back to raw printer.]
  Prop

Test "tutorial/003_arrowType"

Expected: 👍 accept · Size: 626 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

Arrow type (function type)

Test result: 👍 accepted · exit code 0 · wall time: 92 ms · instructions: 389.4 M · max rss memory: 88.6 MB

stdout:
checked 1 declarations

Test "tutorial/004_dependentType"

Expected: 👍 accept · Size: 464 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

Dependent type (forall)

Test result: 👍 accepted · exit code 0 · wall time: 91 ms · instructions: 389.5 M · max rss memory: 88.6 MB

stdout:
checked 1 declarations

Test "tutorial/005_constType"

Expected: 👍 accept · Size: 901 B · Lines: 17 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

Lambda expression

Test result: 👍 accepted · exit code 0 · wall time: 103 ms · instructions: 389.6 M · max rss memory: 88.8 MB

stdout:
checked 1 declarations

Test "tutorial/006_betaReduction"

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

Lambda reduction

Test result: 👍 accepted · exit code 0 · wall time: 122 ms · instructions: 390.1 M · max rss memory: 88.9 MB

stdout:
checked 2 declarations

Test "tutorial/007_betaReduction2"

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

Lambda reduction under binder

Test result: 👍 accepted · exit code 0 · wall time: 98 ms · instructions: 390.0 M · max rss memory: 88.9 MB

stdout:
checked 2 declarations

Test "tutorial/008_forallSortWhnf"

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

The binding domain of a forall may need to be reduce before it is a sort

Test result: 👍 accepted · exit code 0 · wall time: 91 ms · instructions: 389.8 M · max rss memory: 88.8 MB

stdout:
checked 2 declarations

Test "tutorial/009_forallSortBad"

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

The binding domain of a forall has to be a sort

Test result: ✋ rejected · exit code 1 · wall time: 119 ms · instructions: 393.1 M · max rss memory: 89.9 MB

stderr:
uncaught exception: at forallSortBad: (kernel) type expected
  x

Test "tutorial/010_nonTypeType"

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

The type of a declaration has to be a type, not some other expression

Test result: ✋ rejected · exit code 1 · wall time: 95 ms · instructions: 391.9 M · max rss memory: 89.6 MB

stderr:
uncaught exception: at nonTypeType: (kernel) type expected
  constType

Test "tutorial/011_nonPropThm"

Expected: ✋ reject · Size: 428 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

The type of a theorem has to be a proposition

Test result: ✋ rejected · exit code 1 · wall time: 108 ms · instructions: 391.0 M · max rss memory: 89.1 MB

stderr:
uncaught exception: at nonPropThm: (kernel) type of theorem 'nonPropThm' is not a proposition
  Prop

Test "tutorial/012_levelComp1"

Expected: 👍 accept · Size: 395 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

Some level computation

Test result: 👍 accepted · exit code 0 · wall time: 110 ms · instructions: 389.4 M · max rss memory: 88.8 MB

stdout:
checked 1 declarations

Test "tutorial/013_levelComp2"

Expected: 👍 accept · Size: 413 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

Some level computation

Test result: 👍 accepted · exit code 0 · wall time: 103 ms · instructions: 389.3 M · max rss memory: 88.8 MB

stdout:
checked 1 declarations

Test "tutorial/014_levelComp3"

Expected: 👍 accept · Size: 431 B · Lines: 9 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

Some level computation

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

stdout:
checked 1 declarations

Test "tutorial/015_levelParams"

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

Level parameters

Test result: 👍 accepted · exit code 0 · wall time: 137 ms · instructions: 390.1 M · max rss memory: 88.8 MB

stdout:
checked 2 declarations

Test "tutorial/016_tut06_bad01"

Expected: ✋ reject · Size: 431 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

Duplicate universe parameters

Test result: ✋ rejected · exit code 1 · wall time: 136 ms · instructions: 390.8 M · max rss memory: 88.4 MB

stderr:
uncaught exception: at tut06_bad01: (kernel) failed to add declaration to environment, duplicate universe level parameter: 'u'

Test "tutorial/017_levelComp4"

Expected: 👍 accept · Size: 428 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

Some level computation

Test result: 👍 accepted · exit code 0 · wall time: 96 ms · instructions: 389.3 M · max rss memory: 88.8 MB

stdout:
checked 1 declarations

Test "tutorial/018_levelComp5"

Expected: 👍 accept · Size: 428 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

Some level computation

Test result: 👍 accepted · exit code 0 · wall time: 94 ms · instructions: 389.2 M · max rss memory: 88.8 MB

stdout:
checked 1 declarations

Test "tutorial/019_imax1"

Expected: 👍 accept · Size: 813 B · Lines: 16 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

Type inference for forall using imax

Test result: 👍 accepted · exit code 0 · wall time: 103 ms · instructions: 389.5 M · max rss memory: 88.8 MB

stdout:
checked 1 declarations

Test "tutorial/020_imax2"

Expected: 👍 accept · Size: 832 B · Lines: 17 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

Type inference for forall using imax

Test result: 👍 accepted · exit code 0 · wall time: 107 ms · instructions: 389.6 M · max rss memory: 88.8 MB

stdout:
checked 1 declarations

Test "tutorial/021_inferVar"

Expected: 👍 accept · Size: 717 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

Type inference of local variables

Test result: 👍 accepted · exit code 0 · wall time: 141 ms · instructions: 390.0 M · max rss memory: 88.7 MB

stdout:
checked 1 declarations

Test "tutorial/022_defEqLambda"

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

Definitional equality between lambdas

Test result: 👍 accepted · exit code 0 · wall time: 98 ms · instructions: 390.0 M · max rss memory: 88.8 MB

stdout:
checked 1 declarations

Test "tutorial/023_peano1"

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

Peano arithmetic: 2 = 2

Test result: 👍 accepted · exit code 0 · wall time: 104 ms · instructions: 391.5 M · max rss memory: 89.0 MB

stdout:
checked 7 declarations

Test "tutorial/024_peano2"

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

Peano arithmetic: 1 + 1 = 2

Test result: 👍 accepted · exit code 0 · wall time: 102 ms · instructions: 392.4 M · max rss memory: 89.0 MB

stdout:
checked 8 declarations

Test "tutorial/025_peano3"

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

Peano arithmetic: 2 * 2 = 4

Test result: 👍 accepted · exit code 0 · wall time: 115 ms · instructions: 393.3 M · max rss memory: 89.0 MB

stdout:
checked 10 declarations

Test "tutorial/026_letType"

Expected: 👍 accept · Size: 493 B · Lines: 9 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

Type checking a non-dependent let

Test result: 👍 accepted · exit code 0 · wall time: 102 ms · instructions: 389.3 M · max rss memory: 88.8 MB

stdout:
checked 1 declarations

Test "tutorial/027_letTypeDep"

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

Type checking a dependent let

Test result: 👍 accepted · exit code 0 · wall time: 80 ms · instructions: 389.9 M · max rss memory: 88.9 MB

stdout:
checked 3 declarations

Test "tutorial/028_letRed"

Expected: 👍 accept · Size: 631 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

Reducing a let

Test result: 👍 accepted · exit code 0 · wall time: 107 ms · instructions: 389.5 M · max rss memory: 88.9 MB

stdout:
checked 2 declarations

Test "tutorial/029_empty"

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

A simple empty inductive type

Test result: 👍 accepted · exit code 0 · wall time: 116 ms · instructions: 390.3 M · max rss memory: 89.4 MB

stdout:
checked 2 declarations

Test "tutorial/030_boolType"

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

A simple enumeration inductive type

Test result: 👍 accepted · exit code 0 · wall time: 119 ms · instructions: 390.8 M · max rss memory: 89.5 MB

stdout:
checked 2 declarations

Test "tutorial/031_twoBool"

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

A simple product type

Test result: 👍 accepted · exit code 0 · wall time: 115 ms · instructions: 391.9 M · max rss memory: 89.6 MB

stdout:
checked 3 declarations

Test "tutorial/032_andType"

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

A parametrized product type (no level parameters)

Test result: 👍 accepted · exit code 0 · wall time: 100 ms · instructions: 391.6 M · max rss memory: 89.5 MB

stdout:
checked 2 declarations

Test "tutorial/033_prodType"

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

A parametrized product type (with level parameters)

Test result: 👍 accepted · exit code 0 · wall time: 100 ms · instructions: 391.7 M · max rss memory: 89.6 MB

stdout:
checked 2 declarations

Test "tutorial/034_pprodType"

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

A parametrized product type (with more general level parameters)

Test result: 👍 accepted · exit code 0 · wall time: 96 ms · instructions: 391.6 M · max rss memory: 89.6 MB

stdout:
checked 2 declarations

Test "tutorial/035_pUnitType"

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

Level-polymorphic unit type

Test result: 👍 accepted · exit code 0 · wall time: 94 ms · instructions: 390.4 M · max rss memory: 89.5 MB

stdout:
checked 2 declarations

Test "tutorial/036_eqType"

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

Equality, as an important indexed non-recursive data type

Test result: 👍 accepted · exit code 0 · wall time: 110 ms · instructions: 391.3 M · max rss memory: 89.5 MB

stdout:
checked 2 declarations

Test "tutorial/037_natDef"

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

A recursive inductive data type

Test result: 👍 accepted · exit code 0 · wall time: 91 ms · instructions: 391.1 M · max rss memory: 89.6 MB

stdout:
checked 2 declarations

Test "tutorial/038_rbTreeDef"

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

A recursive indexed data type

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

stdout:
checked 4 declarations

Test "tutorial/039_inductBadNonSort"

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

An inductive type with a non-sort type

Test result: ✋ rejected · exit code 1 · wall time: 98 ms · instructions: 392.5 M · max rss memory: 90.0 MB

stderr:
uncaught exception: at inductBadNonSort: (kernel) type expected
  fun x y => x

Test "tutorial/040_inductBadNonSort2"

Expected: ✋ reject · Size: 602 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

Another inductive type with a non-sort type

Test result: ✋ rejected · exit code 1 · wall time: 97 ms · instructions: 391.4 M · max rss memory: 89.9 MB

stderr:
uncaught exception: at inductBadNonSort2: (kernel) type expected
  aType

Test "tutorial/041_inductLevelParam"

Expected: ✋ reject · Size: 519 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

An inductive with duplicate level params

Test result: ✋ rejected · exit code 1 · wall time: 93 ms · instructions: 390.6 M · max rss memory: 88.6 MB

stderr:
uncaught exception: at inductLevelParam: (kernel) failed to add declaration to environment, duplicate universe level parameter: 'u'

Test "tutorial/042_inductTooFewParams"

Expected: ✋ reject · Size: 552 B · Lines: 6 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

An inductive with too few parameters in the type

Test result: ✋ rejected · exit code 1 · wall time: 93 ms · instructions: 390.6 M · max rss memory: 88.6 MB

stderr:
uncaught exception: at inductTooFewParams: (kernel) invalid inductive datatype declaration, incorrect number of parameters

Test "tutorial/043_inductWrongCtorParams"

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

An inductive with a constructor with wrong parameters

Test result: ✋ rejected · exit code 1 · wall time: 100 ms · instructions: 391.3 M · max rss memory: 89.4 MB

stderr:
uncaught exception: at inductWrongCtorParams: (kernel) arg #1 of 'inductWrongCtorParams.mk' does not match inductive datatype parameters

Test "tutorial/044_inductWrongCtorResParams"

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

An inductive with a constructor with wrong parameters in result (they are swapped)

Test result: ✋ rejected · exit code 1 · wall time: 102 ms · instructions: 391.4 M · max rss memory: 89.2 MB

stderr:
uncaught exception: at inductWrongCtorResParams: (kernel) invalid return type for 'inductWrongCtorResParams.mk'

Test "tutorial/045_inductWrongCtorResLevel"

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

An inductive with a constructor with wrong level parameters in result (they are swapped)

Test result: ✋ rejected · exit code 1 · wall time: 102 ms · instructions: 391.4 M · max rss memory: 89.3 MB

stderr:
uncaught exception: at inductWrongCtorResLevel: (kernel) invalid return type for 'inductWrongCtorResLevel.mk'

Test "tutorial/046_inductInIndex"

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

A constructor with an unexpected occurrence of the type in index position of a return type.

Test result: ✋ rejected · exit code 1 · wall time: 107 ms · instructions: 391.3 M · max rss memory: 89.4 MB

stderr:
uncaught exception: at inductInIndex: (kernel) invalid return type for 'inductInIndex.mk'

Test "tutorial/047_indNeg"

Expected: ✋ reject · Size: 1000 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

The classic example of an inductive with negative recursive occurrence

Test result: ✋ rejected · exit code 1 · wall time: 99 ms · instructions: 391.0 M · max rss memory: 89.3 MB

stderr:
uncaught exception: at indNeg: (kernel) arg #1 of 'indNeg.mk' has a non positive occurrence of the datatypes being declared

Test "tutorial/048_reduceCtorParam.mk"

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

When checking inductives, we expect the kernel to reduce the types of constructor arguments.

Test result: 👍 accepted · exit code 0 · wall time: 101 ms · instructions: 392.2 M · max rss memory: 89.6 MB

stdout:
checked 3 declarations

Test "tutorial/049_reduceCtorType.mk"

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

When checking inductives, we expect the kernel to not reduce the type of the constructor itself; that should be all manifest foralls

Test result: ✋ rejected · exit code 1 · wall time: 101 ms · instructions: 391.4 M · max rss memory: 89.4 MB

stderr:
uncaught exception: at reduceCtorType: (kernel) invalid return type for 'reduceCtorType.mk'

Test "tutorial/050_indNegReducible"

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

When checking inductives, we expect the kernel to not reduce the type of the constructor parameters further than head normal form. Recursive occurrences nested inside the head normal form are considered negative occurrences, even if they could be reduced to disappear.

Test result: ✋ rejected · exit code 1 · wall time: 100 ms · instructions: 391.6 M · max rss memory: 89.5 MB

stderr:
uncaught exception: at indNegReducible: (kernel) arg #1 of 'indNegReducible.mk' has a non positive occurrence of the datatypes being declared

Test "tutorial/051_predWithTypeField"

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

An inductive proposition can have constructors with fields of arbitrary level.

Test result: 👍 accepted · exit code 0 · wall time: 115 ms · instructions: 390.5 M · max rss memory: 89.5 MB

stdout:
checked 2 declarations

Test "tutorial/052_typeWithTypeField"

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

An inductive type can have fields of level up to that of the inductive.

Test result: 👍 accepted · exit code 0 · wall time: 92 ms · instructions: 390.5 M · max rss memory: 89.5 MB

stdout:
checked 2 declarations

Test "tutorial/053_typeWithTypeFieldPoly"

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

An inductive type can have fields of level up to that of the inductive (polymorphic variant).

Test result: 👍 accepted · exit code 0 · wall time: 70 ms · instructions: 390.6 M · max rss memory: 89.5 MB

stdout:
checked 2 declarations

Test "tutorial/054_typeWithTooHighTypeField.mk"

Expected: ✋ reject · Size: 947 B · Lines: 11 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

An inductive type can have fields of from higher universes.

Test result: ✋ rejected · exit code 1 · wall time: 69 ms · instructions: 390.9 M · max rss memory: 89.3 MB

stderr:
uncaught exception: at typeWithTooHighTypeField: (kernel) universe level of type_of(arg #1) of 'typeWithTooHighTypeField.mk' is too big for the corresponding inductive datatype

Test "tutorial/055_emptyRec"

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

Asserting the type of the generated recursor

Test result: 👍 accepted · exit code 0 · wall time: 74 ms · instructions: 390.0 M · max rss memory: 89.4 MB

stdout:
checked 2 declarations

Test "tutorial/056_boolRec"

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

Asserting the type of the generated recursor

Test result: 👍 accepted · exit code 0 · wall time: 110 ms · instructions: 391.2 M · max rss memory: 89.5 MB

stdout:
checked 2 declarations

Test "tutorial/057_twoBoolRec"

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

Asserting the type of the generated recursor

Test result: 👍 accepted · exit code 0 · wall time: 118 ms · instructions: 392.3 M · max rss memory: 89.6 MB

stdout:
checked 3 declarations

Test "tutorial/058_andRec"

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

Asserting the type of the generated recursor

Test result: 👍 accepted · exit code 0 · wall time: 121 ms · instructions: 391.5 M · max rss memory: 89.5 MB

stdout:
checked 2 declarations

Test "tutorial/059_prodRec"

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

Asserting the type of the generated recursor

Test result: 👍 accepted · exit code 0 · wall time: 124 ms · instructions: 392.0 M · max rss memory: 89.5 MB

stdout:
checked 2 declarations

Test "tutorial/060_pprodRec"

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

Asserting the type of the generated recursor

Test result: 👍 accepted · exit code 0 · wall time: 124 ms · instructions: 392.0 M · max rss memory: 89.5 MB

stdout:
checked 2 declarations

Test "tutorial/061_punitRec"

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

Asserting the type of the generated recursor

Test result: 👍 accepted · exit code 0 · wall time: 138 ms · instructions: 390.8 M · max rss memory: 89.4 MB

stdout:
checked 2 declarations

Test "tutorial/062_eqRec"

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

Asserting the type of the generated recursor

Test result: 👍 accepted · exit code 0 · wall time: 114 ms · instructions: 391.6 M · max rss memory: 89.5 MB

stdout:
checked 2 declarations

Test "tutorial/063_nRec"

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

Asserting the type of the generated recursor

Test result: 👍 accepted · exit code 0 · wall time: 124 ms · instructions: 391.5 M · max rss memory: 89.5 MB

stdout:
checked 2 declarations

Test "tutorial/064_rbTreeRef"

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

Asserting the type of the generated recursor

Test result: 👍 accepted · exit code 0 · wall time: 123 ms · instructions: 401.0 M · max rss memory: 89.6 MB

stdout:
checked 4 declarations

Test "tutorial/065_boolPropRec"

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

Inductive predicates eliminate into Prop if they have more than one constructor.

Test result: 👍 accepted · exit code 0 · wall time: 106 ms · instructions: 390.6 M · max rss memory: 89.4 MB

stdout:
checked 2 declarations

Test "tutorial/066_existsRec"

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

Inductive predicates eliminate into Prop if they have one constructors and it carries data.

Test result: 👍 accepted · exit code 0 · wall time: 88 ms · instructions: 391.8 M · max rss memory: 89.5 MB

stdout:
checked 2 declarations

Test "tutorial/067_sortElimPropRec"

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

Inductive predicates eliminate into Sort if they have one constructors and it carries data, but the data is known from the type, e.g. a parameter or an index

Test result: 👍 accepted · exit code 0 · wall time: 102 ms · instructions: 392.9 M · max rss memory: 89.6 MB

stdout:
checked 3 declarations

Test "tutorial/068_sortElimProp2Rec"

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

Inductive predicates eliminate into Sort if they have one constructors and it carries data, but the data is known from the type, e.g. a parameter or an index. However, it must occur directly in the result type, with no intervening reduction.

Test result: 👍 accepted · exit code 0 · wall time: 111 ms · instructions: 393.6 M · max rss memory: 89.6 MB

stdout:
checked 4 declarations

Test "tutorial/069_boolRecEqns"

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

Reduction behavior of Bool.rec

Test result: 👍 accepted · exit code 0 · wall time: 119 ms · instructions: 396.3 M · max rss memory: 89.6 MB

stdout:
checked 4 declarations

Test "tutorial/070_prodRecEqns"

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

Reduction behavior of Prod.rec

Test result: 👍 accepted · exit code 0 · wall time: 129 ms · instructions: 396.4 M · max rss memory: 89.6 MB

stdout:
checked 3 declarations

Test "tutorial/071_nRecReduction"

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

A proof relying on the reduction behavior of N.rec

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

stdout:
checked 6 declarations

Test "tutorial/072_listRecReduction"

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

Reduction behavior of List.rec

Test result: 👍 accepted · exit code 0 · wall time: 74 ms · instructions: 402.1 M · max rss memory: 89.8 MB

stdout:
checked 7 declarations

Test "tutorial/073_RBTree.id_spec"

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

Reduction behavior of RBTree.rec

Test result: 👍 accepted · exit code 0 · wall time: 88 ms · instructions: 423.7 M · max rss memory: 89.8 MB

stdout:
checked 7 declarations

Test "tutorial/074_And.right"

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

Type-checking simple projection functions

Test result: 👍 accepted · exit code 0 · wall time: 77 ms · instructions: 391.9 M · max rss memory: 89.5 MB

stdout:
checked 3 declarations

Test "tutorial/075_Prod.snd"

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

Type-checking projection functions with parameters

Test result: 👍 accepted · exit code 0 · wall time: 102 ms · instructions: 392.3 M · max rss memory: 89.6 MB

stdout:
checked 3 declarations

Test "tutorial/076_PProd.snd"

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

Type-checking projection functions

Test result: 👍 accepted · exit code 0 · wall time: 101 ms · instructions: 392.2 M · max rss memory: 89.6 MB

stdout:
checked 3 declarations

Test "tutorial/077_PSigma.snd"

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

Type-checking dependent projection functions

Test result: 👍 accepted · exit code 0 · wall time: 113 ms · instructions: 392.8 M · max rss memory: 89.6 MB

stdout:
checked 3 declarations

Test "tutorial/078_projOutOfRange"

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

Out of range projection

Test result: ✋ rejected · exit code 1 · wall time: 129 ms · instructions: 393.7 M · max rss memory: 90.5 MB

stderr:
uncaught exception: at projOutOfRange: (kernel) invalid projection
  z.3

Test "tutorial/079_projNotStruct"

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

Projection out something that is not a structure

Test result: ✋ rejected · exit code 1 · wall time: 131 ms · instructions: 393.1 M · max rss memory: 90.4 MB

stderr:
uncaught exception: at projNotStruct: (kernel) invalid projection
  x.1

Test "tutorial/080_projProp1"

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

Projecting out of a proposition

The lean kernel allows projections out of propositions if they precede all dependent data fields.

Test result: 👍 accepted · exit code 0 · wall time: 118 ms · instructions: 394.3 M · max rss memory: 89.6 MB

stdout:
checked 4 declarations

Test "tutorial/081_projProp2"

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

Projecting out of a proposition

The lean kernel disallows data projections out of propositional structures.

Test result: ✋ rejected · exit code 1 · wall time: 112 ms · instructions: 395.9 M · max rss memory: 90.5 MB

stderr:
uncaught exception: at projProp2: (kernel) invalid projection
  x.2

Test "tutorial/082_projProp3"

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

Projecting out of a proposition

The lean kernel allows projections out of propositions if they precede all dependent data fields. Non-dependent data fields are not relevant.

Test result: 👍 accepted · exit code 0 · wall time: 112 ms · instructions: 394.2 M · max rss memory: 89.6 MB

stdout:
checked 4 declarations

Test "tutorial/083_projProp4"

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

Projecting out of a proposition

The lean kernel disallows data projections out of propositional structures.

Test result: ✋ rejected · exit code 1 · wall time: 107 ms · instructions: 395.8 M · max rss memory: 90.5 MB

stderr:
uncaught exception: at projProp4: (kernel) invalid projection
  x.4

Test "tutorial/084_projProp5"

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

Projecting out of a proposition

The lean kernel disallows proof projections out of propositional structures that depend on data.

Test result: ✋ rejected · exit code 1 · wall time: 97 ms · instructions: 396.2 M · max rss memory: 90.5 MB

stderr:
uncaught exception: at projProp5: (kernel) invalid projection
  x.4

Test "tutorial/085_projProp6"

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

Projecting out of a proposition.

The lean kernel rejects any projections out of a proposition that come after a dependent data field, even if that is not used by the present projection.

Test result: ✋ rejected · exit code 1 · wall time: 105 ms · instructions: 395.8 M · max rss memory: 90.5 MB

stderr:
uncaught exception: at projProp6: (kernel) invalid projection
  x.6

Test "tutorial/086_projDataIndexRec"

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

The recursor for ProjDataIndex allows elimination into sort.

Test result: 👍 accepted · exit code 0 · wall time: 112 ms · instructions: 393.3 M · max rss memory: 89.6 MB

stdout:
checked 4 declarations

Test "tutorial/087_projIndexData"

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

Projecting out data is not allowed, even if this data appears as an index and the recursor would allow it.

Test result: ✋ rejected · exit code 1 · wall time: 118 ms · instructions: 395.0 M · max rss memory: 90.5 MB

stderr:
uncaught exception: at projIndexData: (kernel) invalid projection
  x.1

Test "tutorial/088_projIndexData2"

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

Projecting out data is not allowed, even if this data appears as an index and the recursor would allow it.

This also forbids projecting out proofs that follow such fields.

Test result: ✋ rejected · exit code 1 · wall time: 92 ms · instructions: 395.0 M · max rss memory: 90.5 MB

stderr:
uncaught exception: at projIndexData2: (kernel) invalid projection
  x.2

Test "tutorial/089_projRed"

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

Projection reductions

Test result: 👍 accepted · exit code 0 · wall time: 118 ms · instructions: 395.8 M · max rss memory: 89.6 MB

stdout:
checked 6 declarations

Test "tutorial/090_ruleK"

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

Rule k for Eq: The recursor reduces even if the major argument is not a constructor, as long replacing the major argument with a constructor is type correct.

Test result: 👍 accepted · exit code 0 · wall time: 124 ms · instructions: 393.3 M · max rss memory: 89.6 MB

stdout:
checked 3 declarations

Test "tutorial/091_ruleKbad"

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

Rule k for Eq should not fire if the types of the major argument do not match that of the constructor.

Test result: ✋ rejected · exit code 1 · wall time: 120 ms · instructions: 612.3 M · max rss memory: 95.5 MB

stderr:
PANIC at _private.Lean.Environment.0.Lean.EnvExtension.getStateImpl Lean.Environment:1341:4: invalid environment extension has been accessed
backtrace:
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(+0x93104ee) [0x55555e8644ee]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lean_panic_fn+0x1c) [0x55555e86497c]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l___private_Lean_Environment_0__Lean_EnvExtension_getStateUnsafe___redArg+0x8f7) [0x55555735fb17]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_ppExprWithInfos+0x17a) [0x555558ebb33a]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_ofExpr___lam__1+0x4e) [0x55555793066e]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lean_apply_2+0x9e9) [0x55555e872149]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x12b) [0x5555579323cb]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6e9) [0x555557932989]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x362) [0x555557932602]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6e9) [0x555557932989]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6d8) [0x555557932978]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6d8) [0x555557932978]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_toString+0x15) [0x555557933535]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_throwKernelException___redArg+0x7fb) [0x555556fd0c0b]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replayConstant___lam__0+0x25) [0x555556fd38e5]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replayConstant+0x2f66) [0x555556fd7f16]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_Std_DTreeMap_Internal_Impl_forInStep___at___00replayConstants_spec__0+0x135) [0x555556fdbbb5]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_Std_DTreeMap_Internal_Impl_forInStep___at___00replayConstants_spec__0+0xde) [0x555556fdbb5e]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replay+0x168) [0x555556fdf7e8]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(_lean_main+0x360) [0x555556fea2b0]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(+0x1a75c92) [0x555556fc9c92]
/nix/store/xx7cm72qy2c0643cm1ipngd87aqwkcdp-glibc-2.40-66/lib/libc.so.6(+0x2a4d8) [0x7ffff7c2a4d8]
/nix/store/xx7cm72qy2c0643cm1ipngd87aqwkcdp-glibc-2.40-66/lib/libc.so.6(__libc_start_main+0x8b) [0x7ffff7c2a59b]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(_start+0x25) [0x555556fcad95]
PANIC at _private.Lean.Environment.0.Lean.EnvExtension.getStateImpl Lean.Environment:1341:4: invalid environment extension has been accessed
backtrace:
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(+0x93104ee) [0x55555e8644ee]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lean_panic_fn+0x1c) [0x55555e86497c]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l___private_Lean_Environment_0__Lean_EnvExtension_getStateUnsafe___redArg+0x8f7) [0x55555735fb17]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_ppExprWithInfos+0x17a) [0x555558ebb33a]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_ofExpr___lam__1+0x4e) [0x55555793066e]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lean_apply_2+0x9e9) [0x55555e872149]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x12b) [0x5555579323cb]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6e9) [0x555557932989]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x362) [0x555557932602]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6e9) [0x555557932989]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_toString+0x15) [0x555557933535]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_throwKernelException___redArg+0x7fb) [0x555556fd0c0b]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replayConstant___lam__0+0x25) [0x555556fd38e5]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replayConstant+0x2f66) [0x555556fd7f16]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_Std_DTreeMap_Internal_Impl_forInStep___at___00replayConstants_spec__0+0x135) [0x555556fdbbb5]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_Std_DTreeMap_Internal_Impl_forInStep___at___00replayConstants_spec__0+0xde) [0x555556fdbb5e]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replay+0x168) [0x555556fdf7e8]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(_lean_main+0x360) [0x555556fea2b0]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(+0x1a75c92) [0x555556fc9c92]
/nix/store/xx7cm72qy2c0643cm1ipngd87aqwkcdp-glibc-2.40-66/lib/libc.so.6(+0x2a4d8) [0x7ffff7c2a4d8]
/nix/store/xx7cm72qy2c0643cm1ipngd87aqwkcdp-glibc-2.40-66/lib/libc.so.6(__libc_start_main+0x8b) [0x7ffff7c2a59b]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(_start+0x25) [0x555556fcad95]
uncaught exception: at ruleKbad: (kernel) declaration type mismatch, 'ruleKbad' has type
  [Error pretty printing expression: (`Inhabited.default` for `IO.Error`). Falling back to raw printer.]
  (Eq.{1} Bool Bool.true Bool.false) -> (forall (a : Bool), Eq.{1} Bool a a)
but it is expected to have type
  [Error pretty printing expression: (`Inhabited.default` for `IO.Error`). Falling back to raw printer.]
  forall (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) (x._@.Tutorial.3161876795._hygCtx._hyg.19 : Eq.{1} Bool Bool.true x._@.Tutorial.3161876795._hygCtx._hyg.17) => Bool) a Bool.false h) a

Test "tutorial/092_ruleKAcc"

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

Rule k should not fire for Acc.

Test result: ✋ rejected · exit code 1 · wall time: 145 ms · instructions: 626.1 M · max rss memory: 95.5 MB

stderr:
PANIC at _private.Lean.Environment.0.Lean.EnvExtension.getStateImpl Lean.Environment:1341:4: invalid environment extension has been accessed
backtrace:
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(+0x93104ee) [0x55555e8644ee]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lean_panic_fn+0x1c) [0x55555e86497c]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l___private_Lean_Environment_0__Lean_EnvExtension_getStateUnsafe___redArg+0x8f7) [0x55555735fb17]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_ppExprWithInfos+0x17a) [0x555558ebb33a]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_ofExpr___lam__1+0x4e) [0x55555793066e]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lean_apply_2+0x9e9) [0x55555e872149]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x12b) [0x5555579323cb]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6e9) [0x555557932989]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x362) [0x555557932602]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6e9) [0x555557932989]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6d8) [0x555557932978]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6d8) [0x555557932978]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_toString+0x15) [0x555557933535]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_throwKernelException___redArg+0x7fb) [0x555556fd0c0b]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replayConstant___lam__0+0x25) [0x555556fd38e5]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replayConstant+0x2f66) [0x555556fd7f16]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_Std_DTreeMap_Internal_Impl_forInStep___at___00replayConstants_spec__0+0x135) [0x555556fdbbb5]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_Std_DTreeMap_Internal_Impl_forInStep___at___00replayConstants_spec__0+0xde) [0x555556fdbb5e]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_Std_DTreeMap_Internal_Impl_forInStep___at___00replayConstants_spec__0+0xde) [0x555556fdbb5e]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replay+0x168) [0x555556fdf7e8]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(_lean_main+0x360) [0x555556fea2b0]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(+0x1a75c92) [0x555556fc9c92]
/nix/store/xx7cm72qy2c0643cm1ipngd87aqwkcdp-glibc-2.40-66/lib/libc.so.6(+0x2a4d8) [0x7ffff7c2a4d8]
/nix/store/xx7cm72qy2c0643cm1ipngd87aqwkcdp-glibc-2.40-66/lib/libc.so.6(__libc_start_main+0x8b) [0x7ffff7c2a59b]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(_start+0x25) [0x555556fcad95]
PANIC at _private.Lean.Environment.0.Lean.EnvExtension.getStateImpl Lean.Environment:1341:4: invalid environment extension has been accessed
backtrace:
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(+0x93104ee) [0x55555e8644ee]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lean_panic_fn+0x1c) [0x55555e86497c]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l___private_Lean_Environment_0__Lean_EnvExtension_getStateUnsafe___redArg+0x8f7) [0x55555735fb17]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_ppExprWithInfos+0x17a) [0x555558ebb33a]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_ofExpr___lam__1+0x4e) [0x55555793066e]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lean_apply_2+0x9e9) [0x55555e872149]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x12b) [0x5555579323cb]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6e9) [0x555557932989]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x362) [0x555557932602]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6e9) [0x555557932989]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_toString+0x15) [0x555557933535]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_throwKernelException___redArg+0x7fb) [0x555556fd0c0b]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replayConstant___lam__0+0x25) [0x555556fd38e5]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replayConstant+0x2f66) [0x555556fd7f16]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_Std_DTreeMap_Internal_Impl_forInStep___at___00replayConstants_spec__0+0x135) [0x555556fdbbb5]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_Std_DTreeMap_Internal_Impl_forInStep___at___00replayConstants_spec__0+0xde) [0x555556fdbb5e]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_Std_DTreeMap_Internal_Impl_forInStep___at___00replayConstants_spec__0+0xde) [0x555556fdbb5e]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replay+0x168) [0x555556fdf7e8]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(_lean_main+0x360) [0x555556fea2b0]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(+0x1a75c92) [0x555556fc9c92]
/nix/store/xx7cm72qy2c0643cm1ipngd87aqwkcdp-glibc-2.40-66/lib/libc.so.6(+0x2a4d8) [0x7ffff7c2a4d8]
/nix/store/xx7cm72qy2c0643cm1ipngd87aqwkcdp-glibc-2.40-66/lib/libc.so.6(__libc_start_main+0x8b) [0x7ffff7c2a59b]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(_start+0x25) [0x555556fcad95]
uncaught exception: at ruleKAcc: (kernel) declaration type mismatch, 'ruleKAcc' has type
  [Error pretty printing expression: (`Inhabited.default` for `IO.Error`). Falling back to raw printer.]
  forall (α : Sort.{u}) (p : α -> α -> Prop) (x : α), (Acc.{u} α p x) -> (forall (a : Bool), Eq.{1} Bool a a)
but it is expected to have type
  [Error pretty printing expression: (`Inhabited.default` for `IO.Error`). Falling back to raw printer.]
  forall (α : Sort.{u}) (p : α -> α -> Prop) (x : α) (h : Acc.{u} α p x) (a : Bool), Eq.{1} Bool (Acc.rec.{1, u} α p (fun (x._@.Tutorial.4255978773._hygCtx._hyg.22 : α) (x._@.Tutorial.4255978773._hygCtx._hyg.24 : Acc.{u} α p x._@.Tutorial.4255978773._hygCtx._hyg.22) => Bool) (fun (x._@.Tutorial.4255978773._hygCtx._hyg.31 : α) (x._@.Tutorial.4255978773._hygCtx._hyg.33 : forall (y : α), (p y x._@.Tutorial.4255978773._hygCtx._hyg.31) -> (Acc.{u} α p y)) (x._@.Tutorial.4255978773._hygCtx._hyg.35 : forall (y : α) (a._@._internal._hyg.0 : p y x._@.Tutorial.4255978773._hygCtx._hyg.31), (fun (x._@.Tutorial.4255978773._hygCtx._hyg.22 : α) (x._@.Tutorial.4255978773._hygCtx._hyg.24 : Acc.{u} α p x._@.Tutorial.4255978773._hygCtx._hyg.22) => Bool) y (x._@.Tutorial.4255978773._hygCtx._hyg.33 y a._@._internal._hyg.0)) => a) x h) a

Test "tutorial/093_aNatLit"

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

Type checking Nat literals

Test result: 👍 accepted · exit code 0 · wall time: 123 ms · instructions: 391.2 M · max rss memory: 89.6 MB

stdout:
checked 2 declarations

Test "tutorial/094_natLitEq"

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

Reducing Nat literals

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

stdout:
checked 3 declarations

Test "tutorial/095_proofIrrelevance"

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

Proof irrelevance

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

stdout:
checked 3 declarations

Test "tutorial/096_unitEta1"

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

Unit eta

Test result: 👍 accepted · exit code 0 · wall time: 96 ms · instructions: 393.1 M · max rss memory: 89.6 MB

stdout:
checked 5 declarations

Test "tutorial/097_unitEta2"

Expected: 👍 accept · Size: 6.0 KB · Lines: 109 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

Unit eta

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

stdout:
checked 4 declarations

Test "tutorial/098_unitEta3"

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

Unit eta

Test result: 👍 accepted · exit code 0 · wall time: 133 ms · instructions: 393.1 M · max rss memory: 89.6 MB

stdout:
checked 4 declarations

Test "tutorial/099_structEta"

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

Structure eta

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

stdout:
checked 7 declarations

Test "tutorial/100_funEta"

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

Function eta for non-dependent functions.

Test result: 👍 accepted · exit code 0 · wall time: 96 ms · instructions: 392.7 M · max rss memory: 89.8 MB

stdout:
checked 3 declarations

Test "tutorial/101_funEtaDep"

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

Function eta for dependent functions (pi types).

Test result: 👍 accepted · exit code 0 · wall time: 82 ms · instructions: 393.1 M · max rss memory: 89.6 MB

stdout:
checked 3 declarations

Test "tutorial/102_funEtaBad"

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

Eta should not identify functions with different bodies.

Test result: ✋ rejected · exit code 1 · wall time: 129 ms · instructions: 611.1 M · max rss memory: 95.5 MB

stderr:
PANIC at _private.Lean.Environment.0.Lean.EnvExtension.getStateImpl Lean.Environment:1341:4: invalid environment extension has been accessed
backtrace:
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(+0x93104ee) [0x55555e8644ee]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lean_panic_fn+0x1c) [0x55555e86497c]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l___private_Lean_Environment_0__Lean_EnvExtension_getStateUnsafe___redArg+0x8f7) [0x55555735fb17]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_ppExprWithInfos+0x17a) [0x555558ebb33a]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_ofExpr___lam__1+0x4e) [0x55555793066e]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lean_apply_2+0x9e9) [0x55555e872149]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x12b) [0x5555579323cb]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6e9) [0x555557932989]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x362) [0x555557932602]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6e9) [0x555557932989]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6d8) [0x555557932978]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6d8) [0x555557932978]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_toString+0x15) [0x555557933535]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_throwKernelException___redArg+0x7fb) [0x555556fd0c0b]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replayConstant___lam__0+0x25) [0x555556fd38e5]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replayConstant+0x2f66) [0x555556fd7f16]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_Std_DTreeMap_Internal_Impl_forInStep___at___00replayConstants_spec__0+0x135) [0x555556fdbbb5]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_Std_DTreeMap_Internal_Impl_forInStep___at___00replayConstants_spec__0+0xde) [0x555556fdbb5e]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replay+0x168) [0x555556fdf7e8]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(_lean_main+0x360) [0x555556fea2b0]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(+0x1a75c92) [0x555556fc9c92]
/nix/store/xx7cm72qy2c0643cm1ipngd87aqwkcdp-glibc-2.40-66/lib/libc.so.6(+0x2a4d8) [0x7ffff7c2a4d8]
/nix/store/xx7cm72qy2c0643cm1ipngd87aqwkcdp-glibc-2.40-66/lib/libc.so.6(__libc_start_main+0x8b) [0x7ffff7c2a59b]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(_start+0x25) [0x555556fcad95]
PANIC at _private.Lean.Environment.0.Lean.EnvExtension.getStateImpl Lean.Environment:1341:4: invalid environment extension has been accessed
backtrace:
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(+0x93104ee) [0x55555e8644ee]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lean_panic_fn+0x1c) [0x55555e86497c]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l___private_Lean_Environment_0__Lean_EnvExtension_getStateUnsafe___redArg+0x8f7) [0x55555735fb17]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_ppExprWithInfos+0x17a) [0x555558ebb33a]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_ofExpr___lam__1+0x4e) [0x55555793066e]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lean_apply_2+0x9e9) [0x55555e872149]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x12b) [0x5555579323cb]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6e9) [0x555557932989]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x362) [0x555557932602]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6e9) [0x555557932989]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_toString+0x15) [0x555557933535]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_throwKernelException___redArg+0x7fb) [0x555556fd0c0b]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replayConstant___lam__0+0x25) [0x555556fd38e5]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replayConstant+0x2f66) [0x555556fd7f16]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_Std_DTreeMap_Internal_Impl_forInStep___at___00replayConstants_spec__0+0x135) [0x555556fdbbb5]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_Std_DTreeMap_Internal_Impl_forInStep___at___00replayConstants_spec__0+0xde) [0x555556fdbb5e]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replay+0x168) [0x555556fdf7e8]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(_lean_main+0x360) [0x555556fea2b0]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(+0x1a75c92) [0x555556fc9c92]
/nix/store/xx7cm72qy2c0643cm1ipngd87aqwkcdp-glibc-2.40-66/lib/libc.so.6(+0x2a4d8) [0x7ffff7c2a4d8]
/nix/store/xx7cm72qy2c0643cm1ipngd87aqwkcdp-glibc-2.40-66/lib/libc.so.6(__libc_start_main+0x8b) [0x7ffff7c2a59b]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(_start+0x25) [0x555556fcad95]
uncaught exception: at funEtaBad: (kernel) declaration type mismatch, 'funEtaBad' has type
  [Error pretty printing expression: (`Inhabited.default` for `IO.Error`). Falling back to raw printer.]
  forall (x._@.Tutorial.4249243883._hygCtx._hyg.28 : Type) (x._@.Tutorial.4249243883._hygCtx._hyg.30 : Type), (x._@.Tutorial.4249243883._hygCtx._hyg.28 -> x._@.Tutorial.4249243883._hygCtx._hyg.28) -> (forall (f : x._@.Tutorial.4249243883._hygCtx._hyg.28 -> x._@.Tutorial.4249243883._hygCtx._hyg.30), Eq.{1} (x._@.Tutorial.4249243883._hygCtx._hyg.28 -> x._@.Tutorial.4249243883._hygCtx._hyg.30) f f)
but it is expected to have type
  [Error pretty printing expression: (`Inhabited.default` for `IO.Error`). Falling back to raw printer.]
  forall (α : Type) (β : Type) (g : α -> α) (f : α -> β), Eq.{1} (α -> β) (fun (x : α) => f (g x)) f

Test "tutorial/103_etaRuleK"

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

Corner case for function eta: Does a defeq between a partially applied recursor with rule k and a free variable trigger eta expansion?

Taking the official kernel as the specification, the answer is no. See https://github.com/leanprover/lean4/issues/12520 for a discussion.

Test result: ✋ rejected · exit code 1 · wall time: 127 ms · instructions: 602.4 M · max rss memory: 95.5 MB

stderr:
PANIC at _private.Lean.Environment.0.Lean.EnvExtension.getStateImpl Lean.Environment:1341:4: invalid environment extension has been accessed
backtrace:
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(+0x93104ee) [0x55555e8644ee]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lean_panic_fn+0x1c) [0x55555e86497c]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l___private_Lean_Environment_0__Lean_EnvExtension_getStateUnsafe___redArg+0x8f7) [0x55555735fb17]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_ppExprWithInfos+0x17a) [0x555558ebb33a]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_ofExpr___lam__1+0x4e) [0x55555793066e]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lean_apply_2+0x9e9) [0x55555e872149]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x12b) [0x5555579323cb]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6e9) [0x555557932989]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x362) [0x555557932602]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6e9) [0x555557932989]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6d8) [0x555557932978]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6d8) [0x555557932978]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_toString+0x15) [0x555557933535]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_throwKernelException___redArg+0x7fb) [0x555556fd0c0b]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replayConstant___lam__0+0x25) [0x555556fd38e5]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replayConstant+0x3332) [0x555556fd82e2]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_Std_DTreeMap_Internal_Impl_forInStep___at___00replayConstants_spec__0+0x135) [0x555556fdbbb5]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replay+0x168) [0x555556fdf7e8]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(_lean_main+0x360) [0x555556fea2b0]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(+0x1a75c92) [0x555556fc9c92]
/nix/store/xx7cm72qy2c0643cm1ipngd87aqwkcdp-glibc-2.40-66/lib/libc.so.6(+0x2a4d8) [0x7ffff7c2a4d8]
/nix/store/xx7cm72qy2c0643cm1ipngd87aqwkcdp-glibc-2.40-66/lib/libc.so.6(__libc_start_main+0x8b) [0x7ffff7c2a59b]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(_start+0x25) [0x555556fcad95]
PANIC at _private.Lean.Environment.0.Lean.EnvExtension.getStateImpl Lean.Environment:1341:4: invalid environment extension has been accessed
backtrace:
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(+0x93104ee) [0x55555e8644ee]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lean_panic_fn+0x1c) [0x55555e86497c]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l___private_Lean_Environment_0__Lean_EnvExtension_getStateUnsafe___redArg+0x8f7) [0x55555735fb17]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_ppExprWithInfos+0x17a) [0x555558ebb33a]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_ofExpr___lam__1+0x4e) [0x55555793066e]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lean_apply_2+0x9e9) [0x55555e872149]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x12b) [0x5555579323cb]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6e9) [0x555557932989]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x362) [0x555557932602]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6e9) [0x555557932989]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_toString+0x15) [0x555557933535]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_throwKernelException___redArg+0x7fb) [0x555556fd0c0b]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replayConstant___lam__0+0x25) [0x555556fd38e5]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replayConstant+0x3332) [0x555556fd82e2]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_Std_DTreeMap_Internal_Impl_forInStep___at___00replayConstants_spec__0+0x135) [0x555556fdbbb5]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replay+0x168) [0x555556fdf7e8]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(_lean_main+0x360) [0x555556fea2b0]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(+0x1a75c92) [0x555556fc9c92]
/nix/store/xx7cm72qy2c0643cm1ipngd87aqwkcdp-glibc-2.40-66/lib/libc.so.6(+0x2a4d8) [0x7ffff7c2a4d8]
/nix/store/xx7cm72qy2c0643cm1ipngd87aqwkcdp-glibc-2.40-66/lib/libc.so.6(__libc_start_main+0x8b) [0x7ffff7c2a59b]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(_start+0x25) [0x555556fcad95]
uncaught exception: at etaRuleK: (kernel) declaration type mismatch, 'etaRuleK' has type
  [Error pretty printing expression: (`Inhabited.default` for `IO.Error`). Falling back to raw printer.]
  forall (a : (Eq.{1} Bool Bool.true Bool.true) -> Bool), Eq.{1} ((Eq.{1} Bool Bool.true Bool.true) -> Bool) a a
but it is expected to have type
  [Error pretty printing expression: (`Inhabited.default` for `IO.Error`). Falling back to raw printer.]
  forall (a : (Eq.{1} Bool Bool.true Bool.true) -> Bool), Eq.{1} ((Eq.{1} Bool Bool.true Bool.true) -> Bool) (Eq.rec.{1, 1} Bool Bool.true (fun (x._@.Tutorial.2477593770._hygCtx._hyg.31 : Bool) (x._@.Tutorial.2477593770._hygCtx._hyg.33 : Eq.{1} Bool Bool.true x._@.Tutorial.2477593770._hygCtx._hyg.31) => Bool) (a (Eq.refl.{1} Bool Bool.true)) Bool.true) a

Test "tutorial/104_etaCtor"

Expected: ✋ reject · Size: 9.0 KB · Lines: 148 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

Corner case for function eta: Does a defeq between a partially applied constructor trigger eta expansion?

Taking the official kernel as the specification, the answer is no. See https://github.com/leanprover/lean4/issues/12520 for a discussion.

Test result: ✋ rejected · exit code 1 · wall time: 122 ms · instructions: 603.6 M · max rss memory: 95.5 MB

stderr:
PANIC at _private.Lean.Environment.0.Lean.EnvExtension.getStateImpl Lean.Environment:1341:4: invalid environment extension has been accessed
backtrace:
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(+0x93104ee) [0x55555e8644ee]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lean_panic_fn+0x1c) [0x55555e86497c]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l___private_Lean_Environment_0__Lean_EnvExtension_getStateUnsafe___redArg+0x8f7) [0x55555735fb17]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_ppExprWithInfos+0x17a) [0x555558ebb33a]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_ofExpr___lam__1+0x4e) [0x55555793066e]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lean_apply_2+0x9e9) [0x55555e872149]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x12b) [0x5555579323cb]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6e9) [0x555557932989]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x362) [0x555557932602]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6e9) [0x555557932989]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6d8) [0x555557932978]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6d8) [0x555557932978]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_toString+0x15) [0x555557933535]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_throwKernelException___redArg+0x7fb) [0x555556fd0c0b]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replayConstant___lam__0+0x25) [0x555556fd38e5]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replayConstant+0x3332) [0x555556fd82e2]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_Std_DTreeMap_Internal_Impl_forInStep___at___00replayConstants_spec__0+0x135) [0x555556fdbbb5]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replay+0x168) [0x555556fdf7e8]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(_lean_main+0x360) [0x555556fea2b0]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(+0x1a75c92) [0x555556fc9c92]
/nix/store/xx7cm72qy2c0643cm1ipngd87aqwkcdp-glibc-2.40-66/lib/libc.so.6(+0x2a4d8) [0x7ffff7c2a4d8]
/nix/store/xx7cm72qy2c0643cm1ipngd87aqwkcdp-glibc-2.40-66/lib/libc.so.6(__libc_start_main+0x8b) [0x7ffff7c2a59b]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(_start+0x25) [0x555556fcad95]
PANIC at _private.Lean.Environment.0.Lean.EnvExtension.getStateImpl Lean.Environment:1341:4: invalid environment extension has been accessed
backtrace:
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(+0x93104ee) [0x55555e8644ee]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lean_panic_fn+0x1c) [0x55555e86497c]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l___private_Lean_Environment_0__Lean_EnvExtension_getStateUnsafe___redArg+0x8f7) [0x55555735fb17]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_ppExprWithInfos+0x17a) [0x555558ebb33a]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_ofExpr___lam__1+0x4e) [0x55555793066e]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lean_apply_2+0x9e9) [0x55555e872149]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x12b) [0x5555579323cb]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6e9) [0x555557932989]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x362) [0x555557932602]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6e9) [0x555557932989]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_toString+0x15) [0x555557933535]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_throwKernelException___redArg+0x7fb) [0x555556fd0c0b]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replayConstant___lam__0+0x25) [0x555556fd38e5]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replayConstant+0x3332) [0x555556fd82e2]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_Std_DTreeMap_Internal_Impl_forInStep___at___00replayConstants_spec__0+0x135) [0x555556fdbbb5]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replay+0x168) [0x555556fdf7e8]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(_lean_main+0x360) [0x555556fea2b0]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(+0x1a75c92) [0x555556fc9c92]
/nix/store/xx7cm72qy2c0643cm1ipngd87aqwkcdp-glibc-2.40-66/lib/libc.so.6(+0x2a4d8) [0x7ffff7c2a4d8]
/nix/store/xx7cm72qy2c0643cm1ipngd87aqwkcdp-glibc-2.40-66/lib/libc.so.6(__libc_start_main+0x8b) [0x7ffff7c2a59b]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(_start+0x25) [0x555556fcad95]
uncaught exception: at etaCtor: (kernel) declaration type mismatch, 'etaCtor' has type
  [Error pretty printing expression: (`Inhabited.default` for `IO.Error`). Falling back to raw printer.]
  forall (x : True -> T), Eq.{1} (True -> T) x x
but it is expected to have type
  [Error pretty printing expression: (`Inhabited.default` for `IO.Error`). Falling back to raw printer.]
  forall (x : True -> T), Eq.{1} (True -> T) (T.mk (T.val (x True.intro))) x

Test "tutorial/105_reflOccLeft"

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

Rejection: recursive occurrence on the left of an arrow, behind further arrows inside a constructor argument.

The constructor argument is a function type Nat → (I → Nat).

Test result: ✋ rejected · exit code 1 · wall time: 91 ms · instructions: 392.4 M · max rss memory: 89.4 MB

stderr:
uncaught exception: at reflOccLeft: (kernel) arg #1 of 'reflOccLeft.mk' has a non positive occurrence of the datatypes being declared

Test "tutorial/106_reflOccInIndex"

Expected: ✋ reject · Size: 4.0 KB · Lines: 66 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

Rejection: recursive occurrence in index position, behind a further arrow.

We build an indexed inductive I : Type → Type with a constructor argument Nat → I (I α), so the recursive occurrence appears as an index argument.

Test result: ✋ rejected · exit code 1 · wall time: 98 ms · instructions: 394.0 M · max rss memory: 90.5 MB

stderr:
uncaught exception: at reflOccInIndex: (kernel) application type mismatch
  reflOccInIndex x
argument has type
  Nat
but function has type
  Type → Type

Test "tutorial/107_reduceCtorParamRefl.mk"

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

When checking inductives, we expect the kernel to reduce the types of constructor arguments in all positive positions.

Test result: 👍 accepted · exit code 0 · wall time: 120 ms · instructions: 392.3 M · max rss memory: 89.6 MB

stdout:
checked 3 declarations

Test "tutorial/108_reduceCtorParamRefl2.mk"

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

When checking inductives, we expect the kernel to reduce the types of constructor arguments in all positive positions.

Test result: 👍 accepted · exit code 0 · wall time: 98 ms · instructions: 392.3 M · max rss memory: 89.6 MB

stdout:
checked 3 declarations

Test "tutorial/109_rTreeRec"

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

Asserting the type of the generated recursor.

Test result: 👍 accepted · exit code 0 · wall time: 95 ms · instructions: 392.5 M · max rss memory: 89.6 MB

stdout:
checked 3 declarations

Test "tutorial/110_rtreeRecReduction"

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

Reduction behavior of RTree.rec on RTree.mk.

Test result: 👍 accepted · exit code 0 · wall time: 101 ms · instructions: 396.0 M · max rss memory: 89.8 MB

stdout:
checked 6 declarations

Test "tutorial/111_accRecType"

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

Asserting the type of Acc.rec.

Test result: 👍 accepted · exit code 0 · wall time: 103 ms · instructions: 394.2 M · max rss memory: 89.6 MB

stdout:
checked 2 declarations

Test "tutorial/112_accRecReduction"

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

Acc.rec reduces on Acc.intro.

Test result: 👍 accepted · exit code 0 · wall time: 96 ms · instructions: 398.7 M · max rss memory: 89.6 MB

stdout:
checked 4 declarations

Test "tutorial/113_accRecNoEta"

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

Acc.rec does not have structure eta.

Test result: ✋ rejected · exit code 1 · wall time: 119 ms · instructions: 626.1 M · max rss memory: 95.5 MB

stderr:
PANIC at _private.Lean.Environment.0.Lean.EnvExtension.getStateImpl Lean.Environment:1341:4: invalid environment extension has been accessed
backtrace:
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(+0x93104ee) [0x55555e8644ee]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lean_panic_fn+0x1c) [0x55555e86497c]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l___private_Lean_Environment_0__Lean_EnvExtension_getStateUnsafe___redArg+0x8f7) [0x55555735fb17]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_ppExprWithInfos+0x17a) [0x555558ebb33a]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_ofExpr___lam__1+0x4e) [0x55555793066e]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lean_apply_2+0x9e9) [0x55555e872149]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x12b) [0x5555579323cb]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6e9) [0x555557932989]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x362) [0x555557932602]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6e9) [0x555557932989]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6d8) [0x555557932978]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6d8) [0x555557932978]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_toString+0x15) [0x555557933535]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_throwKernelException___redArg+0x7fb) [0x555556fd0c0b]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replayConstant___lam__0+0x25) [0x555556fd38e5]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replayConstant+0x2f66) [0x555556fd7f16]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_Std_DTreeMap_Internal_Impl_forInStep___at___00replayConstants_spec__0+0x135) [0x555556fdbbb5]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_Std_DTreeMap_Internal_Impl_forInStep___at___00replayConstants_spec__0+0xde) [0x555556fdbb5e]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_Std_DTreeMap_Internal_Impl_forInStep___at___00replayConstants_spec__0+0xde) [0x555556fdbb5e]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replay+0x168) [0x555556fdf7e8]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(_lean_main+0x360) [0x555556fea2b0]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(+0x1a75c92) [0x555556fc9c92]
/nix/store/xx7cm72qy2c0643cm1ipngd87aqwkcdp-glibc-2.40-66/lib/libc.so.6(+0x2a4d8) [0x7ffff7c2a4d8]
/nix/store/xx7cm72qy2c0643cm1ipngd87aqwkcdp-glibc-2.40-66/lib/libc.so.6(__libc_start_main+0x8b) [0x7ffff7c2a59b]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(_start+0x25) [0x555556fcad95]
PANIC at _private.Lean.Environment.0.Lean.EnvExtension.getStateImpl Lean.Environment:1341:4: invalid environment extension has been accessed
backtrace:
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(+0x93104ee) [0x55555e8644ee]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lean_panic_fn+0x1c) [0x55555e86497c]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l___private_Lean_Environment_0__Lean_EnvExtension_getStateUnsafe___redArg+0x8f7) [0x55555735fb17]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_ppExprWithInfos+0x17a) [0x555558ebb33a]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_ofExpr___lam__1+0x4e) [0x55555793066e]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lean_apply_2+0x9e9) [0x55555e872149]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x12b) [0x5555579323cb]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6e9) [0x555557932989]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x362) [0x555557932602]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x6e9) [0x555557932989]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(l_Lean_MessageData_toString+0x15) [0x555557933535]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_throwKernelException___redArg+0x7fb) [0x555556fd0c0b]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replayConstant___lam__0+0x25) [0x555556fd38e5]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replayConstant+0x2f66) [0x555556fd7f16]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_Std_DTreeMap_Internal_Impl_forInStep___at___00replayConstants_spec__0+0x135) [0x555556fdbbb5]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_Std_DTreeMap_Internal_Impl_forInStep___at___00replayConstants_spec__0+0xde) [0x555556fdbb5e]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_Std_DTreeMap_Internal_Impl_forInStep___at___00replayConstants_spec__0+0xde) [0x555556fdbb5e]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(lp_lean4lean_replay+0x168) [0x555556fdf7e8]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(_lean_main+0x360) [0x555556fea2b0]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(+0x1a75c92) [0x555556fc9c92]
/nix/store/xx7cm72qy2c0643cm1ipngd87aqwkcdp-glibc-2.40-66/lib/libc.so.6(+0x2a4d8) [0x7ffff7c2a4d8]
/nix/store/xx7cm72qy2c0643cm1ipngd87aqwkcdp-glibc-2.40-66/lib/libc.so.6(__libc_start_main+0x8b) [0x7ffff7c2a59b]
/actions-runner/_work/lean-kernel-arena/lean-kernel-arena/_build/checkers/lean4lean/src/d29406d/.lake/build/bin/lean4lean(_start+0x25) [0x555556fcad95]
uncaught exception: at accRecNoEta: (kernel) declaration type mismatch, 'accRecNoEta' has type
  [Error pretty printing expression: (`Inhabited.default` for `IO.Error`). Falling back to raw printer.]
  forall (α : Type) (r : α -> α -> Prop) (a : α), (Acc.{1} α r a) -> (forall (p : Bool), Eq.{1} Bool p p)
but it is expected to have type
  [Error pretty printing expression: (`Inhabited.default` for `IO.Error`). Falling back to raw printer.]
  forall {α : Type} (r : α -> α -> Prop) (a : α) (h : Acc.{1} α r a) (p : Bool), Eq.{1} Bool (Acc.rec.{1, 1} α r (fun (x._@.Tutorial.4017164079._hygCtx._hyg.22 : α) (x._@.Tutorial.4017164079._hygCtx._hyg.24 : Acc.{1} α r x._@.Tutorial.4017164079._hygCtx._hyg.22) => Bool) (fun (x._@.Tutorial.4017164079._hygCtx._hyg.31 : α) (x._@.Tutorial.4017164079._hygCtx._hyg.33 : forall (y : α), (r y x._@.Tutorial.4017164079._hygCtx._hyg.31) -> (Acc.{1} α r y)) (x._@.Tutorial.4017164079._hygCtx._hyg.35 : forall (y : α) (a._@._internal._hyg.0 : r y x._@.Tutorial.4017164079._hygCtx._hyg.31), (fun (x._@.Tutorial.4017164079._hygCtx._hyg.22 : α) (x._@.Tutorial.4017164079._hygCtx._hyg.24 : Acc.{1} α r x._@.Tutorial.4017164079._hygCtx._hyg.22) => Bool) y (x._@.Tutorial.4017164079._hygCtx._hyg.33 y a._@._internal._hyg.0)) => p) a h) p

Test "tutorial/114_quotMkType"

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

Asserting the type of Quot.mk.

Test result: 👍 accepted · exit code 0 · wall time: 102 ms · instructions: 392.7 M · max rss memory: 89.5 MB

stdout:
checked 3 declarations

Test "tutorial/115_quotIndType"

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

Asserting the type of Quot.ind.

Test result: 👍 accepted · exit code 0 · wall time: 98 ms · instructions: 393.0 M · max rss memory: 89.5 MB

stdout:
checked 3 declarations

Test "tutorial/116_quotLiftType"

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

Asserting the type of Quot.lift.

Test result: 👍 accepted · exit code 0 · wall time: 99 ms · instructions: 392.9 M · max rss memory: 89.5 MB

stdout:
checked 3 declarations

Test "tutorial/117_quotSoundType"

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

Asserting the type of Quot.sound.

Test result: 👍 accepted · exit code 0 · wall time: 72 ms · instructions: 393.4 M · max rss memory: 89.5 MB

stdout:
checked 4 declarations

Test "tutorial/118_quotLiftReduction"

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

Reduction behavior of Quot.lift on Quot.mk.

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

stdout:
checked 3 declarations

Test "tutorial/119_quotIndReduction"

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

Reduction behavior of Quot.ind on Quot.mk.

Test result: 👍 accepted · exit code 0 · wall time: 86 ms · instructions: 394.3 M · max rss memory: 89.6 MB

stdout:
checked 3 declarations

Test "tutorial/120_dup_defs"

Expected: ✋ reject · Size: 479 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

Two definitions with the same name

Test result: ✋ rejected · exit code 1 · wall time: 85 ms · instructions: 389.2 M · max rss memory: 88.3 MB

stderr:
uncaught exception: Duplicate declaration: dup_defs

Test "tutorial/121_dup_ind_def"

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

A definition and a constructor with the same name

Test result: ✋ rejected · exit code 1 · wall time: 92 ms · instructions: 389.6 M · max rss memory: 88.4 MB

stderr:
uncaught exception: Duplicate declaration: dup_ind_def

Test "tutorial/122_dup_ctor_def"

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

A definition and a constructor with the same name

Test result: ✋ rejected · exit code 1 · wall time: 70 ms · instructions: 389.6 M · max rss memory: 88.4 MB

stderr:
uncaught exception: Duplicate declaration: dup_ctor_def.mk

Test "tutorial/123_dup_rec_def"

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

A definition and a recursor with the same name

Test result: ✋ rejected · exit code 1 · wall time: 92 ms · instructions: 389.7 M · max rss memory: 88.4 MB

stderr:
uncaught exception: Duplicate declaration: dup_rec_def.rec

Test "tutorial/124_dup_rec_def2"

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

A definition with the name of a recursor, and the recursor named differently. This would pass simple checks for duplicate definitions in the parser, but should still be rejected by the checker.

Test result: ✋ rejected · exit code 1 · wall time: 97 ms · instructions: 391.6 M · max rss memory: 89.5 MB

stderr:
uncaught exception: at dup_rec_def2: (kernel) constant has already been declared 'dup_rec_def2.rec'

Test "tutorial/125_dup_ctor_rec"

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

A constructor and a recursor with the same name

Test result: ✋ rejected · exit code 1 · wall time: 91 ms · instructions: 389.9 M · max rss memory: 88.4 MB

stderr:
uncaught exception: Duplicate declaration: dup_ctor_rec.rec

Test "tutorial/126_DupConCon"

Expected: ✋ reject · Size: 2.2 KB · Lines: 35 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source

An inductive with two constructors with the same name

Test result: ✋ rejected · exit code 1 · wall time: 99 ms · instructions: 390.2 M · max rss memory: 88.4 MB

stderr:
uncaught exception: Duplicate declaration: dup_ind_con_con.mk