Lean Kernel Arena / kiota

Version: 0.1.0 · 📄 Declaration · 🔗 Source

Test "bogus1"

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

Test result: ✋ rejected · exit code 1 · wall time: 41 ms · instructions: 5.6 M · max rss memory: 8.8 MB

stderr:

REJECT: [thm] theorem 43: value type does not match declared type

Test "cedar"

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

Test result: ✋ rejected · exit code 1 · wall time: 17.6 s · instructions: 241.6 G · max rss memory: 1.3 GB

stderr:

[decl #100] theorem Nat.le.brecOn
[decl #200] def UInt8.ofNat
[decl #300] theorem Nat.le_add_right
[decl #400] def String.toByteArray
[decl #500] def DecidableRel
[decl #600] def UInt64.toBitVec
[decl #700] def _private.Init.Data.Nat.Lemmas.0.Nat.shiftRight_succ_inside.match_1_1
[decl #800] theorem Nat.exists_ge_and_testBit_of_ge_two_pow
[decl #900] def Nat.Linear.Var.denote
[decl #1000] def UInt8.land
[decl #1100] def _private.Init.Data.Nat.Lemmas.0.Nat.add_right_cancel_iff.match_1_1
[decl #1200] def _private.Init.Data.Int.Lemmas.0.Int.negSucc_ne_zero.match_1_1
[decl #1300] def Lean.Omega.Constraint.div
[decl #1400] theorem Lean.Omega.IntList.gcd_cons_div_right
[decl #1500] def _private.Init.Data.Int.DivMod.Bootstrap.0.Int.emod_add_mul_ediv.match_1_1
[decl #1600] theorem _private.Init.Data.BitVec.Bootstrap.0.BitVec.getLsbD_of_ge._proof_1_3
[decl #1700] def Nat.digitChar
[decl #1800] def BitVec.instHShiftLeftNat
[decl #1900] theorem Std.IsLinearOrder.toIsLinearPreorder
[decl #2000] theorem _private.Init.Data.Int.Pow.0.Int.pow_succ._simp_1_2
[decl #2100] theorem _private.Init.Data.Nat.Bitwise.Lemmas.0.Nat.le_of_testBit._proof_1_1
[decl #2200] def Array.foldl
[decl #2300] theorem BitVec.getLsbD_shiftLeft
[decl #2400] def _private.Init.Data.Nat.MinMax.0.Nat.min_comm.match_1_1
[decl #2500] theorem List.length_append
[decl #2600] theorem BitVec.getElem_cast._proof_2
[decl #2700] theorem eq_comm
[decl #2800] theorem _private.Init.Data.String.Decode.0.utf8DecodeChar?_eq_assemble₂._proof_1
[decl #2900] theorem _private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.toBitVec_eq_of_parseFirstByte_eq_twoMore
[decl #3000] theorem _private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.assemble₄_eq_some_iff_utf8EncodeChar_eq._simp_1_12
[decl #3100] theorem _private.Init.Data.String.Decode.0.utf8DecodeChar?_append_eq_assemble₃._proof_1
[decl #3200] theorem List.utf8DecodeChar?_utf8Encode_singleton_append
REJECT: [Cedar.Spec.Value._sizeOf_5_eq] application argument type mismatch

Test "constlevels"

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

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

stderr:

REJECT: [_test] let value type mismatch

Test "cslib"

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

Test result: ✋ rejected · exit code 1 · wall time: 2.9 m · instructions: 2.8 T · max rss memory: 5.3 GB

stderr:

[decl #100] def Nat.le.below.casesOn
[decl #200] def _private.Init.Prelude.0.Nat.pow_pos.match_1_1
[decl #300] def NonUnitalNonAssocSemiring.toMul
[decl #400] def Function.comp
[decl #500] def Finset.val
[decl #600] def EmptyCollection.emptyCollection
[decl #700] theorem instDecidableIff._proof_1
[decl #800] def MonoidWithZero.toMulZeroOneClass
[decl #900] def Function.Injective.addCommMagma
[decl #1000] theorem MonoidHom.instFunLike._proof_1
[decl #1100] theorem RingHomInvPair.ids
[decl #1200] theorem le_sup_inf
[decl #1300] theorem or_self
[decl #1400] def CompleteBooleanAlgebra.toCompleteLattice
[decl #1500] theorem Prop.instBooleanAlgebra._proof_6
[decl #1600] def Acc.recOn
[decl #1700] def panicCore
[decl #1800] theorem Lean.Data.AC.Context.sort_loop_nonEmpty
[decl #1900] theorem Function.LeftInverse.eq_rightInverse
[decl #2000] def Iff.eq
[decl #2100] theorem WithTop.addZeroClass._proof_2
[decl #2200] theorem not_iff_comm
[decl #2300] theorem Countable.of_equiv
[decl #2400] theorem _private.Init.Data.List.Pairwise.0.List.pairwise_map._simp_1_1
[decl #2500] theorem exists_and_right
[decl #2600] def _private.Init.Data.NeZero.0.instNeZeroNatHAdd.match_5
[decl #2700] def Int.casesOn
[decl #2800] theorem Int.subNatNat_sub
[decl #2900] def Int.ediv
[decl #3000] theorem Nat.modCore_eq
[decl #3100] theorem Int.dvd_refl
[decl #3200] theorem _private.Init.Omega.IntList.0.Lean.Omega.IntList.gcd_eq_zero._simp_1_1
[decl #3300] def Lean.Omega.LinearCombo.add
[decl #3400] theorem List.findIdx_cons
[decl #3500] def Int.Linear.hugeFuel
[decl #3600] theorem Int.Linear.eq_diseq_subst
[decl #3700] def Lean.Grind.Semiring.natCast
[decl #3800] def Lean.Grind.CommRing.Poly.below
[decl #3900] def Nat.Linear.ExprCnstr.denote
[decl #4000] def Lean.Grind.CommRing.Mon.mul.go.match_1
[decl #4100] theorem Lean.Grind.AddCommMonoid.add_comm
[decl #4200] theorem Lean.Grind.Semiring.pow_succ
[decl #4300] theorem Lean.Grind.CommRing.instBEqMon.beq.eq_1
[decl #4400] theorem Lean.Grind.CommRing.instBEqPoly.beq.eq_3
[decl #4500] theorem Finite.of_equiv
[decl #4600] def List.replicate
[decl #4700] theorem List.find?_eq_none
[decl #4800] theorem exists_exists_and_eq_and
[decl #4900] theorem le_compl_compl
[decl #5000] theorem Finset.mk_cons
[decl #5100] theorem Std.DTreeMap.Internal.Impl.insert._proof_10
[decl #5200] theorem Std.DTreeMap.Internal.Impl.balance!.match_1.congr_eq_1
[decl #5300] theorem Std.DTreeMap.Internal.Impl.balanceₘ.match_1.congr_eq_1
[decl #5400] theorem Std.DTreeMap.Internal.Impl.balanceR!.fun_cases_unfolding
[decl #5500] theorem Std.DTreeMap.Internal.Impl.minView._proof_23
[decl #5600] theorem Std.DTreeMap.Internal.Impl.alter._proof_18
[decl #5700] def instSizeOfDefault
[decl #5800] theorem Std.DTreeMap.Internal.Impl.link._proof_18
[decl #5900] theorem Std.DTreeMap.Internal.Impl.applyCell._proof_4
[decl #6000] def Std.DTreeMap.Internal.Cell.noConfusion
[decl #6100] theorem _private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.toListModel_filter_lt_of_lt._simp_1_2
[decl #6200] theorem Std.DTreeMap.Internal.Impl.updateCell._proof_58
[decl #6300] theorem Std.DTreeMap.Internal.Impl.Const.alter.eq_2
[decl #6400] theorem Std.DTreeMap.Internal.Impl.ordered_mergeWith
[decl #6500] theorem Std.Internal.List.DistinctKeys.tail
[decl #6600] def Lean.Name.casesOn
[decl #6700] theorem Nat.zero_shiftRight
[decl #6800] theorem Nat.mul_left_cancel_iff
[decl #6900] theorem BitVec.getElem_and
[decl #7000] def BitVec.instOfNat
[decl #7100] def ByteArray.instAppend
[decl #7200] theorem _private.Init.Data.BitVec.Lemmas.0.BitVec.shiftLeft_add._proof_1_1
[decl #7300] theorem Array.foldl_toList
[decl #7400] theorem _private.Init.Data.String.Decode.0.String.utf8EncodeChar_eq_utf8EncodeCharFast._proof_1_10
[decl #7500] theorem Array.getElem_append
[decl #7600] theorem BitVec.toNat_of_zero_length
[decl #7700] def Nat.shiftLeft_bitwise_distrib._auto_5
[decl #7800] theorem _private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.isInvalidContinuationByte_getElem_utf8EncodeChar_one_of_utf8Size_eq_four
[decl #7900] theorem _private.Init.Data.String.Decode.0.utf8DecodeChar?_append_eq_assemble₄
[decl #8000] def String.decEq.match_1
[decl #8100] def Std.DHashMap.Internal.AssocList.casesOn
[decl #8200] def _private.Std.Data.DHashMap.Internal.AssocList.Basic.0.Std.DHashMap.Internal.AssocList.filter.go._f
[decl #8300] def _private.Lean.Expr.0.Lean.instBEqMVarId.beq.match_1
[decl #8400] def instMaxUInt32
[decl #8500] def Std.TreeMap.inner
[decl #8600] def Lean.NameMap.instEmptyCollection
[decl #8700] theorem _private.Init.Data.String.Basic.0.String.Pos.Raw.isValidUTF8_extract_iff._simp_1_2
[decl #8800] theorem String.Pos.Raw.IsValid.le_rawEndPos
[decl #8900] theorem String.Pos.Raw.isValidUTF8_extract_iff
[decl #9000] theorem String.Pos.Raw.IsValidForSlice.le_rawEndPos
[decl #9100] theorem String.Slice.endPos_copy
[decl #9200] theorem _private.Init.Data.String.Basic.0.String.Pos.Raw.IsValid.append_left._simp_1_2
[decl #9300] def Std.IteratorLoop.rel
[decl #9400] def Lean.Name.isPrefixOf
[decl #9500] theorem String.Slice.slice._proof_1
[decl #9600] def Lean.privateHeader
[decl #9700] def Lean.Core.Context.quotContext
[decl #9800] def Lean.ReducibilityStatus.casesOn
[decl #9900] def Lean.ExprStructEq.instBEq
[decl #10000] def UInt64.lor
[decl #10100] def _private.Lean.Data.PersistentHashMap.0.Lean.PersistentHashMap.insert.match_1
[decl #10200] def Lean.instInhabitedSyntax
[decl #10300] def _private.Lean.Meta.LitValues.0.Lean.Meta.getNatValue?.match_1
[decl #10400] theorem Array.reverse.loop._unary._proof_3
[decl #10500] def _private.Std.Data.DHashMap.Internal.Defs.0.Std.DHashMap.Internal.Raw₀.get.match_1
[decl #10600] theorem LawfulHashable.hash_eq
[decl #10700] theorem Std.DHashMap.Internal.Raw.WFImp.size_eq
[decl #10800] theorem Std.DHashMap.Internal.Raw₀.eraseₘaux.eq_1
[decl #10900] theorem UInt64.toNat_toUSize
[decl #11000] theorem Std.Internal.List.getValue?_append_of_containsKey_eq_false
[decl #11100] theorem left_inv_eq_right_inv
[decl #11200] theorem Filter.HasBasis.tendsto_right_iff
[decl #11300] theorem IsOrderedMonoid.mul_le_mul_right
[decl #11400] def instTransIff
[decl #11500] def Lean.LocalContext.getUnusedName
[decl #11600] def Units.instDivInvMonoid
[decl #11700] def Std.ExtDTreeMap.Const.modify
[decl #11800] theorem _private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.minEntry?ₘ_eq_minEntry?._simp_1_1
[decl #11900] theorem Std.LawfulOrderMin.toMinEqOr
[decl #12000] def LinearOrder.min_def._autoParam
[decl #12100] def Pi.instAdd
[decl #12200] def Ordering.Compares.match_1
[decl #12300] theorem Ring.toNonUnitalRing._proof_4
[decl #12400] theorem AddCancelCommMonoid.toIsLeftCancelAdd
[decl #12500] theorem IsAbsoluteValue.abv_mul'
[decl #12600] theorem DivisionRing.isDomain
[decl #12700] theorem Nat.instIsStrictOrderedRing
[decl #12800] theorem Int.cast_natCast
[decl #12900] theorem Pi.mulZeroOneClass._proof_3
[decl #13000] theorem Nat.eq_of_mul_eq_mul_left
[decl #13100] theorem _private.Init.Data.Int.DivMod.Lemmas.0.Int.natAbs_ediv._proof_1_3
[decl #13200] theorem Rat.mul._proof_1
[decl #13300] theorem _private.Init.Data.Rat.Lemmas.0.Rat.divInt_eq_divInt_iff._simp_1_2
[decl #13400] theorem Rat.inv._proof_3
[decl #13500] theorem _private.Init.Data.Rat.Lemmas.0.Rat.lt_iff._proof_1_2
[decl #13600] theorem Function.Involutive.eq_iff
[decl #13700] theorem OrderIso.map_sup
[decl #13800] def CommRing.toGrindCommRing
[decl #13900] theorem _private.Mathlib.Data.Real.Basic.0.Real.wrapped._proof_1._@.Mathlib.Data.Real.Basic.1138242547._hygCtx._hyg.8
[decl #14000] def Lean.Grind.Linarith.Poly.denote'
[decl #14100] def Lean.Grind.Linarith.Expr.norm
[decl #14200] theorem CauSeq.instPreorderAbs._proof_3
[decl #14300] theorem CauSeq.le_of_eq_of_le
[decl #14400] theorem GaloisCoinsertion.liftCompleteLattice._proof_1
[decl #14500] theorem Function.Surjective.forall₂
[decl #14600] theorem Function.Surjective.mulOneClass._proof_4
[decl #14700] theorem NonUnitalRing.mul_assoc
[decl #14800] theorem CauSeq.Completion.Cauchy.divisionRing._proof_2
[decl #14900] theorem Rat.cast_one
[decl #15000] theorem Int.negSucc_add_negSucc
[decl #15100] def OrderEmbedding.ofMapLEIff
[decl #15200] theorem Nat.gc_ceil_coe
[decl #15300] theorem Commute.neg_left_iff
[decl #15400] theorem SeminormedCommRing.toNonUnitalSeminormedCommRing._proof_11
[decl #15500] theorem Multiset.le_cons_erase
[decl #15600] theorem Multiset.coe_fold_l
[decl #15700] theorem List.bagInter._sparseCasesOn_1.else_eq
[decl #15800] theorem Finset.fold_union_inter
[decl #15900] theorem Finset.sdiff_eq_filter
[decl #16000] theorem Filter.Tendsto.prodMk_nhds
[decl #16100] theorem compl_le_iff_compl_le
[decl #16200] theorem uniformContinuous_neg
[decl #16300] theorem WithTop.le_def'
[decl #16400] theorem ENNReal.instAddCommMonoidWithOne._proof_11
[decl #16500] theorem Option.mem_def
[decl #16600] def WithTop.instMulZeroOneClass
[decl #16700] theorem CompletelyDistribLattice.le_himp_iff
[decl #16800] theorem OrderIso.isLUB_preimage'
[decl #16900] theorem NNReal.instConditionallyCompleteLinearOrderBot._proof_12
[decl #17000] theorem WithTop.instCompleteLinearOrder._proof_5
[decl #17100] theorem _private.Mathlib.Order.Interval.Set.Defs.0.Set.Ioo._simp_2
[decl #17200] theorem Nonneg.coe_inv
[decl #17300] theorem le_iff_exists_add
[decl #17400] def Lean.Grind.AC.Expr.toSeq'.match_1
[decl #17500] theorem WithTop.add_eq_top._simp_1
[decl #17600] theorem dist_nonneg
[decl #17700] theorem edist_add_add_le
[decl #17800] theorem Metric.uniformity_eq_comap_nhds_zero
[decl #17900] theorem Filter.Eventually.and
[decl #18000] theorem _private.Mathlib.Order.Filter.Map.0.Filter.principal_singleton._simp_1_1
[decl #18100] theorem Set.BijOn.mapsTo
[decl #18200] def Pairwise
[decl #18300] theorem OrderTopology.to_orderClosedTopology
[decl #18400] theorem iSup_inf_eq
[decl #18500] theorem continuousAt_const
[decl #18600] theorem Filter.tendsto_map
[decl #18700] theorem isClosed_Iic
[decl #18800] theorem Multiset.coe_bind
[decl #18900] theorem ContinuousSub.continuous_sub
[decl #19000] theorem Set.range_eq_singleton
[decl #19100] def pseudoEMetricSpacePi
[decl #19200] theorem Finset.prod_erase_mul
[decl #19300] theorem norm_eq_zero
[decl #19400] def RingCon.instPartialOrder
[decl #19500] theorem Set.instIsNonstrictStrictOrderSubsetSSubset
[decl #19600] theorem tsub_eq_zero_of_le
[decl #19700] theorem norm_sub_rev
[decl #19800] theorem Filter.pure_le_principal
[decl #19900] theorem Vector.mk.inj
[decl #20000] theorem AddSubgroup.neg_mem'
[decl #20100] def instLTFloat
[decl #20200] def _private.Lean.Meta.Basic.0.Lean.Meta.mkFreshExprMVarImpl
[decl #20300] def _private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.toNatLit?.match_1
[decl #20400] def Lean.Meta.ConfigWithKey._private_1
[decl #20500] def Lean.getOutParamPositions?
[decl #20600] def instMonadControlStateRefT'._aux_1
[decl #20700] def Std.IterStep.ctorElim
[decl #20800] theorem Std.Rxc.LawfulHasSize.size_eq_succ_of_succ?_eq_some
[decl #20900] def _private.Lean.Data.PersistentArray.0.Lean.PersistentArray.forIn.match_1
[decl #21000] theorem Submonoid.copy._proof_2
[decl #21100] theorem FreeAlgebra.instAlgebra._proof_1
[decl #21200] def LinearMapClass
[decl #21300] def AddSubmonoid.instMin.match_1
[decl #21400] theorem Subsemiring.toSemiring._proof_3
[decl #21500] theorem Real.normedField._proof_11
[decl #21600] theorem Rat.lt_of_le_of_ne
[decl #21700] theorem Nat.cast_add_one
[decl #21800] theorem RingHomCompTriple.ids
[decl #21900] theorem inner_eq_zero_symm
[decl #22000] theorem mul_mul_mul_comm
[decl #22100] theorem isPreconnected_empty
[decl #22200] theorem Topology.IsInducing.continuous_iff
[decl #22300] theorem add_left_inj
[decl #22400] def Int8.casesOn
[decl #22500] theorem AddSubmonoid.instCompleteLattice._proof_1
[decl #22600] theorem Std.DTreeMap.Internal.Impl.maxKey.induct_unfolding
[decl #22700] def String._sizeOf_inst
[decl #22800] theorem Finsupp.sum_hom_add_index
[decl #22900] def Matrix
[decl #23000] def Lean.Meta.Grind.instBEqPreInstance.match_1
[decl #23100] def Lean.Meta.Sym.instHashableAlphaKey
[decl #23200] theorem Finset.mem_of_mem_inter_left
[decl #23300] theorem pow_mod_orderOf
[decl #23400] theorem List.Disjoint.symm
[decl #23500] theorem Equiv.equivCongr._proof_5
[decl #23600] theorem Int.emod_emod
[decl #23700] def _private.Mathlib.Data.Fintype.Defs.0.Fintype.subsingleton.match_1
[decl #23800] def Trunc.liftOn
[decl #23900] theorem SemiconjBy.inv_right_iff._simp_2
[decl #24000] theorem forall_prop_of_false
[decl #24100] theorem Std.DTreeMap.Internal.Impl.minKey!_eq_minKey!
[decl #24200] theorem Equiv.prodPUnit._proof_1
[decl #24300] theorem Cardinal.commSemiring._proof_11
[decl #24400] theorem instCommSemiringENat._proof_17
[decl #24500] theorem Set.pairwise_singleton
[decl #24600] def SuccOrder.ofCore
[decl #24700] theorem _private.Mathlib.SetTheory.Cardinal.ENat.0.Cardinal.toENat._simp_1
[decl #24800] theorem Filter.Tendsto.congr'
[decl #24900] theorem Finset.mem_preimage
[decl #25000] theorem mul_lt_mul_of_pos'
[decl #25100] theorem Finset.sum_nonneg
[decl #25200] def Set.uniqueSingleton
[decl #25300] theorem mem_closure_iff_nhds_ne_bot
[decl #25400] theorem Set.Nonempty.some.congr_simp
[decl #25500] theorem mul_invOf_cancel_right'
[decl #25600] theorem _private.Mathlib.Topology.Algebra.InfiniteSum.ENNReal.0.ENNReal.hasSum_coe._simp_1_2
[decl #25700] theorem cauchy_iff_exists_le_nhds
[decl #25800] def _private.Mathlib.Order.Filter.CountablyGenerated.0.Filter.exists_antitone_seq.match_1_1
[decl #25900] theorem le_of_tendsto_of_tendsto
[decl #26000] theorem ENNReal.instT5Space
[decl #26100] theorem Lean.Grind.CommRing.Mon.denote.match_1.congr_eq_1
[decl #26200] theorem sInf_lt_iff
[decl #26300] theorem pairwise_on_bool
[decl #26400] theorem Finset.insert_eq_of_mem
[decl #26500] theorem Finset.le_inf
[decl #26600] theorem MeasureTheory.Measure.trim_le
[decl #26700] theorem _private.Mathlib.Data.Set.Insert.0.Set.insert_subset_iff._proof_1_1
[decl #26800] theorem MeasureTheory.measure_congr
[decl #26900] def eventuallyMeasurableSpace
[decl #27000] theorem aeSeq.iSup
REJECT: [MeasureTheory.OuterMeasure.addCommMonoid._proof_2] theorem 183722: value type does not match declared type

Test "ctor-num-fields"

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

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

stderr:

REJECT: [_private.Test.0.S.f] projection index out of range

Test "extra-rec"

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

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

stderr:

REJECT: recursor `rogue` is not named `I.rec` for an inductive in this group

Test "init"

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

Test result: ✋ rejected · exit code 1 · wall time: 2.9 m · instructions: 2.0 T · max rss memory: 11.9 GB

stderr:

[decl #100] theorem Eq.symm
[decl #200] theorem Nat.pow_pos
[decl #300] def inferInstance
[decl #400] def _private.Init.Core.0.dif_neg.match_1_1
[decl #500] def instNatCastInt
[decl #600] theorem Nat.not_le
[decl #700] def Lean.Omega.normalize?.match_1
[decl #800] theorem Int.dvd_mul_right
[decl #900] theorem Nat.add_mul_div_right
[decl #1000] theorem Int.natCast_nonneg
[decl #1100] def _private.Init.Data.Int.Lemmas.0.Int.neg_eq_neg_one_mul.match_1_1
[decl #1200] def instDecidableOr
[decl #1300] theorem of_decide_eq_false
[decl #1400] theorem LawfulApplicative.toLawfulFunctor
[decl #1500] theorem Array.ext'
[decl #1600] theorem imp_false._simp_1
[decl #1700] def Std.IsLinearPreorder.of_le._auto_1
[decl #1800] theorem Std.PRange.instLawfulUpwardEnumerableLTNat
[decl #1900] def Fin.instOfNat
[decl #2000] theorem String.Pos.Raw.le_iff
[decl #2100] def Std.Packages.LinearOrderOfLEArgs.max_eq._autoParam
[decl #2200] theorem String.Pos.Raw.instLinearOrderPackage._proof_5
[decl #2300] def _private.Init.Data.Nat.Lemmas.0.Nat.zero_shiftRight.match_1_1
[decl #2400] theorem Nat.Linear.Poly.denote_append
[decl #2500] theorem _private.Init.Data.Nat.Bitwise.Lemmas.0.Nat.testBit_two_pow_mul._simp_1_1
[decl #2600] def Lean.Grind.CommRing.Poly.mulMon_nc
[decl #2700] def List.decidableBEx.match_3
[decl #2800] def ByteArray.instGetElemNatUInt8LtSize
[decl #2900] theorem Nat.min_eq_right
[decl #3000] def BitVec.shiftLeftZeroExtend
[decl #3100] theorem _private.Init.Data.Nat.Lemmas.0.Nat.succ_mod_succ_eq_zero_iff._simp_1_3
[decl #3200] theorem _private.Init.Data.Nat.Bitwise.Lemmas.0.Nat.le_of_testBit._proof_1_1
[decl #3300] theorem _private.Init.Data.String.Decode.0.utf8Size_le_of_utf8DecodeChar?_eq_some._proof_1_3
[decl #3400] theorem Char.utf8Size_eq_four_iff
[decl #3500] theorem List.cons_ne_self._simp_1
[decl #3600] theorem String.utf8EncodeCharFast.fun_cases_unfolding
[decl #3700] theorem _private.Init.Data.String.Decode.0.utf8DecodeChar?_eq_assemble₂
[decl #3800] theorem _private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.assemble₃_eq_some_iff_utf8EncodeChar_eq._proof_1_5
[decl #3900] theorem _private.Init.Data.Array.Extract.0.Array.extract_eq_self_iff._proof_1_2
[decl #4000] theorem ByteArray.append_assoc
[decl #4100] def _private.Init.Data.String.Defs.0.String.Pos.Raw.isValid_iff_isValidUTF8_extract_zero.match_1_3
[decl #4200] theorem String.Pos.Raw.IsValidForSlice.isValid_offsetBy
[decl #4300] theorem Int.neg_eq_comm
[decl #4400] def Lean.Grind.Semiring.natCast
[decl #4500] def Array.swap._auto_1
[decl #4600] theorem Array.getElem_push_lt._proof_3
[decl #4700] def ForInStep.casesOn
[decl #4800] theorem _private.Init.Prelude.0.System.Platform.getNumBits._proof_1
[decl #4900] theorem _private.Init.Data.Range.Polymorphic.Iterators.0.Std.Rxo.Iterator.upwardEnumerableLe_of_isPlausibleIndirectOutput._simp_1_4
[decl #5000] theorem Int.ediv_nonneg
[decl #5100] theorem _private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.instLawfulUpwardEnumerable
[decl #5200] theorem _private.Init.Data.BitVec.Lemmas.0.BitVec.toInt_sub._proof_1_1
[decl #5300] theorem Int.emod_eq_of_lt
[decl #5400] def BitVec.instRxcHasSize
[decl #5500] theorem BitVec.msb_eq_decide
[decl #5600] theorem Int8.eq_iff_toBitVec_eq
[decl #5700] theorem Int.emod_pos_of_not_dvd
[decl #5800] def Rat.numDenCasesOn''
[decl #5900] theorem and_congr_right_iff
[decl #6000] theorem UInt64.neg_one_or
[decl #6100] theorem List.findFinIdx?._proof_1
[decl #6200] theorem Lean.Grind.Linarith.Expr.intMul.inj
[decl #6300] theorem _private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rcc.getElem?_toList_eq._simp_1_2
[decl #6400] theorem Nat.dvd_mul_left_of_dvd
[decl #6500] theorem List.pmap_congr_left
[decl #6600] theorem compareOfLessAndEq_eq_swap_of_lt_iff_not_gt_and_ne
[decl #6700] def _private.Init.Data.List.Nat.TakeDrop.0.List.length_take.match_1_1
[decl #6800] theorem Rat.mkRat_eq_iff
[decl #6900] theorem Std.IterM.step_filterMapM
[decl #7000] theorem _private.Init.Data.String.OrderInstances.0.String.Pos.Raw.instTotalLe._simp_2
[decl #7100] theorem String.Slice.utf8ByteSize_sliceFrom
[decl #7200] theorem String.Pos.next._proof_2
[decl #7300] def RandomGen.mk.noConfusion
[decl #7400] theorem _private.Init.Data.BitVec.Lemmas.0.BitVec.toInt_neg_of_ne_intMin._proof_1_3
[decl #7500] theorem Nat.decidableBallLT._proof_1
[decl #7600] def Option.pfilter.match_1
[decl #7700] def _private.Init.Data.List.Sublist.0.List.sublist_append_right.match_1_1
[decl #7800] theorem _private.Init.Data.String.Termination.0.String.Slice.Pos.lt_iff_remainingBytes_lt._simp_1_2
[decl #7900] def Lean.Grind.IntModule.OfNatModule.Q.mk
[decl #8000] theorem _private.Init.Data.Iterators.Combinators.Monadic.Take.0.Std.IterM.take.surjective_of_zero_lt._proof_1_2
[decl #8100] theorem Nat.Coprime.coprime_div_left
[decl #8200] theorem _private.Init.Data.BitVec.Lemmas.0.BitVec.msb_allOnes._proof_1_1
[decl #8300] theorem _private.Init.Data.BitVec.Lemmas.0.BitVec.toInt_one._proof_1_2
[decl #8400] theorem USize.toNat_mod_size
[decl #8500] theorem Array.getElem_map._proof_1
[decl #8600] theorem _private.Init.Data.String.PosRaw.0.String.Pos.Raw.le_trans._simp_1_1
[decl #8700] def String.instDecidableLePos_1
[decl #8800] def String.front
[decl #8900] def instDecidableIte
[decl #9000] theorem _private.Init.Data.Range.Polymorphic.BitVec.0.BitVec.instRxcLawfulHasSize._simp_1
[decl #9100] theorem Array.forIn_yield_eq_foldlM
[decl #9200] theorem UInt32.succMany?_ofBitVec
[decl #9300] theorem _private.Init.Data.Array.Basic.0.Array.back._proof_1
[decl #9400] def MonadReader.read
[decl #9500] def prec(_)
[decl #9600] def Std.Roc.Sliceable.noConfusionType
[decl #9700] theorem List.append_eq_append_iff
[decl #9800] theorem Std.Iterators.ProductivenessRelation.wf
[decl #9900] theorem _private.Init.Data.List.Range.0.List.mem_range'._simp_1_9
[decl #10000] opaque UInt64.toFloat
[decl #10100] theorem List.find?_some
[decl #10200] def Vector.flatMap
[decl #10300] def instLEISize
[decl #10400] theorem Array.mem_of_ne_of_mem
[decl #10500] theorem Nat.succ_max_succ
[decl #10600] def Lean.ParserDescr.noConfusion
[decl #10700] def Lean.Data.AC.Expr.brecOn.go
[decl #10800] def Std.Iter.isEmpty
[decl #10900] theorem Nat.toList_ric_succ
[decl #11000] def Lean.Grind.CommRing.Poly.mul.go
[decl #11100] theorem Lean.Grind.CommRing.Mon.mul.go.match_3.congr_eq_1
[decl #11200] theorem Lean.Grind.CommRing.norm_int
[decl #11300] theorem UInt8.toUSize._proof_2
[decl #11400] theorem Lean.Grind.Linarith.instBEqPoly.beq.eq_def
[decl #11500] theorem Lean.Grind.CommRing.instBEqPoly.beq.eq_1
[decl #11600] theorem Array.getElem?_extract_of_lt
[decl #11700] theorem _private.Init.Data.Array.Basic.0.Array.eraseIdx._unary._proof_3
[decl #11800] theorem List.length_zipIdx
[decl #11900] def IO.FS.Mode.ctorIdx
[decl #12000] theorem _private.Init.Data.Range.Polymorphic.UInt.0.USize.instLawfulHasSize._simp_2
[decl #12100] theorem Nat.size_rco
[decl #12200] def Std.Ric.HasRcoIntersection.casesOn
[decl #12300] theorem Std.IterM.DefaultConsumers.forIn'_eq_wf
[decl #12400] theorem Std.Rxc.Iterator.isPlausibleIndirectOutput_iff
[decl #12500] def Fin.instXorOp
[decl #12600] theorem Vector.getElem_push_eq
[decl #12700] theorem ISize.toInt_inj
[decl #12800] def FloatArray.casesOn
[decl #12900] theorem Option.mem_def
[decl #13000] def instMonadEIO._aux_1
[decl #13100] theorem Vector.mem_range'
[decl #13200] def CoeSort.noConfusionType
[decl #13300] theorem Int64.mul_comm
[decl #13400] def Std.Iterators.ProductivenessRelation.casesOn
[decl #13500] def String.Pos.ofSliceFrom
[decl #13600] def List.zip
[decl #13700] def Array.swapAt!
[decl #13800] theorem Int.getElem_toList_roo
[decl #13900] def Int32.toInt8
[decl #14000] def BitVec.uppcRec.match_1
[decl #14100] theorem UInt8.instLawfulUpwardEnumerable
[decl #14200] def Lean.Grind.CommRing.Expr.neg.noConfusion
[decl #14300] def Std.Legacy.Range.forIn'
[decl #14400] def StateCpsT.lift
[decl #14500] theorem _private.Init.Data.SInt.Lemmas.0.Int64.toInt_ofNat_of_lt._proof_1_2
[decl #14600] theorem _private.Init.Data.BitVec.Lemmas.0.BitVec.reverse_append._proof_1_1
[decl #14700] def _private.Init.Meta.Defs.0.Lean.Name.needsNoEscapeAscii
[decl #14800] theorem _private.Init.Data.String.Pattern.String.0.String.Slice.Pattern.ForwardSliceSearcher.buildTable.computeDistance._unary._proof_1
[decl #14900] theorem Std.Rxc.Iterator.instLawfulIteratorLoop
[decl #15000] theorem Lean.Grind.rfl_true
[decl #15100] theorem _private.Init.Data.Fin.Lemmas.0.Fin.reverseInduction._proof_4
[decl #15200] def _private.Init.Data.Sum.Basic.0.Sum.lex_inr_inl.match_1_1
[decl #15300] theorem List.append_eq_append_iff_of_size_eq_left
[decl #15400] theorem _private.Init.Data.String.Pattern.String.0.String.Slice.Pattern.ForwardSliceSearcher.buildTable.go._unary._proof_16
[decl #15500] theorem String.Slice.Pos.Splits.pos_eq
[decl #15600] theorem _private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch.partialMatch_iff
[decl #15700] theorem _private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.isTable_buildTable._proof_1_2
[decl #15800] theorem List.pmap_eq_nil_iff._simp_1
[decl #15900] theorem Lean.Grind.imp_eq
[decl #16000] theorem List.minIdxOn_eq_iff_eq_minOn
[decl #16100] theorem Vector.toList_zip
[decl #16200] theorem List.le_toArray
[decl #16300] def Option.max
[decl #16400] theorem Nat.sub_lt_of_lt
[decl #16500] theorem Lean.Grind.IsCharP.ofNat_eq_zero_iff
[decl #16600] def Lean.Grind.Ring.OfSemiring.natCast
[decl #16700] theorem Dyadic.ofOdd_eq_ofIntWithPrec
[decl #16800] theorem String.append_eq_empty_iff
[decl #16900] def Std.Roi.toArray
[decl #17000] theorem Vector.attach_map
[decl #17100] theorem Nat.Coprime.gcd_mul_right_cancel_right
[decl #17200] def Lean.Syntax.instToStringTSyntax
[decl #17300] def Vector.countP
[decl #17400] def String.Slice.RevSplitIterator._sizeOf_1
[decl #17500] theorem String.Pos.lt_trans
[decl #17600] def List.eraseDups
[decl #17700] theorem Int.sub_nonpos_of_le
[decl #17800] theorem Int.Linear.diseq_coeff
[decl #17900] theorem _private.Init.Util.0.withPtrEqDecEq._proof_1
[decl #18000] def instSliceableSubarrayNat_3
[decl #18100] theorem _private.Init.Data.Int.DivMod.Lemmas.0.Int.ediv_ediv_of_pos
[decl #18200] theorem _private.Init.Data.Dyadic.Basic.0.Dyadic.blt_iff_toRat._simp_1_8
[decl #18300] theorem Int.Linear.Poly.mul'.eq_1
[decl #18400] theorem USize.add_zero
[decl #18500] def UInt16._sizeOf_inst
[decl #18600] def BitVec.DivModArgs.n
[decl #18700] theorem _private.Init.Data.Range.Polymorphic.SInt.0.Int16.toBitVec_minValueSealed_eq_intMinSealed
[decl #18800] theorem _private.Init.Data.Range.Polymorphic.Fin.0.Fin.instLawfulHasSize._proof_2
[decl #18900] theorem _private.Init.Data.BitVec.Lemmas.0.BitVec.getMsbD_extractLsb._proof_1_1
[decl #19000] def Array.qpartition._auto_3
[decl #19100] theorem BitVec.eq_of_zero_length
[decl #19200] def Std.MaxEqOr.elim
[decl #19300] theorem Option.filter_pfilter
[decl #19400] theorem Lean.Grind.instAddRightCancelNat
[decl #19500] theorem _private.Init.WFComputable.0.Acc.recC._unary._proof_8
[decl #19600] theorem _private.Init.Data.Array.Lemmas.0.Array.map_eq_append_iff._simp_1_2
[decl #19700] theorem Sum.Lex.mono
[decl #19800] theorem Lean.Grind.CommRing.Poly.mulMonC_nc.go.eq_def
[decl #19900] theorem MonadAttach.attach_bind_eq_pbind
[decl #20000] theorem List.take_subset
[decl #20100] def _private.Init.Data.List.Impl.0.List.takeWhileTR.go.match_1
[decl #20200] def FloatArray.noConfusion
[decl #20300] theorem Lean.Grind.CommRing.Expr.denote_toPolyC
[decl #20400] theorem Array.reverse_eq_append_iff
[decl #20500] def String.Slice.Pos.Down._sizeOf_1
[decl #20600] theorem Array.findIdx_le_size
[decl #20700] theorem List.mapFinIdx_eq_cons_iff._proof_2
[decl #20800] opaque IO.initializing
[decl #20900] theorem Int8.toInt64_ofInt
[decl #21000] theorem BitVec.ofNat_eq_ofNat
[decl #21100] theorem Subtype.instTotalLE
[decl #21200] theorem _private.Init.Data.Nat.Fold.0.Nat.dfold._proof_8
[decl #21300] theorem _private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Ric.mem_toList_iff_mem._simp_1_2
[decl #21400] theorem Dyadic.add_mul
[decl #21500] theorem Function.LeftInverse.id
[decl #21600] theorem Array.mem_eraseP_of_neg
[decl #21700] theorem _private.Init.Data.BitVec.Lemmas.0.BitVec.toInt_add_of_not_saddOverflow._proof_1_6
[decl #21800] def _private.Init.Data.Nat.Control.0.Nat.anyM.loop
[decl #21900] def StateRefT'.instMonad._aux_13
[decl #22000] theorem List.toList_mkSlice_roo
[decl #22100] theorem UInt16.zero_div
[decl #22200] theorem List.findFinIdx?_eq_some_iff
[decl #22300] theorem USize.toFin_mod
[decl #22400] theorem UInt8.toNat_mul
[decl #22500] theorem Array.any_append'
[decl #22600] theorem List.of_concat_eq_concat
[decl #22700] theorem _private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.splitRevAt_go
[decl #22800] def Substring.Raw.all
[decl #22900] theorem String.Slice.Pos.next_induction
[decl #23000] theorem Int16.not_or_self
[decl #23100] def _private.Init.Data.Int.DivMod.Lemmas.0.Int.tmod_lt_of_pos.match_1_1
[decl #23200] theorem Lean.Grind.CommRing.Poly.denoteS_concat
[decl #23300] theorem Lean.Grind.CommRing.Poly.insert_Nonneg
[decl #23400] theorem ListSlice.size_eq_length_toList
[decl #23500] theorem List.isEqv_toArray
[decl #23600] theorem _private.Init.Data.Array.Perm.0.List.perm_iff_toArray_perm._simp_1_1
[decl #23700] theorem Vector.getElem_insertIdx_of_gt._proof_4
[decl #23800] def Except.toOption
[decl #23900] theorem _private.Init.Data.Array.BinSearch.0.Array.binSearchAux._unary._proof_5
[decl #24000] theorem instLawfulCommIdentityInt32HAndNegOfNat
[decl #24100] def String.Slice.Pattern.BackwardSliceSearcher.endsWith
[decl #24200] theorem _private.Init.Data.Range.Polymorphic.IntLemmas.0.Int.getElem!_toArray_rco._simp_1_1
[decl #24300] def Std.Format.FlattenBehavior._sizeOf_1
[decl #24400] theorem Nat.log2_two_pow
[decl #24500] theorem Int.dvd_emod_add_of_dvd_add
[decl #24600] theorem List.findIdx_eq_length_of_false
[decl #24700] theorem Std.LawfulOrderMax.of_max_le_iff
[decl #24800] theorem _private.Init.Data.List.ToArray.0.Array.takeWhile.go.eq_1
[decl #24900] def StateRefT'.run
[decl #25000] theorem Int.neg_mul_tmod_right
[decl #25100] theorem _private.Init.Data.Range.Polymorphic.SInt.0.Int16.instRxiHasSize_eq._simp_1_3
[decl #25200] theorem Vector.getElem_pop'
[decl #25300] theorem Int.Linear.diseq_split
[decl #25400] opaque IO.Process.Child.takeStdin
[decl #25500] def Char.instHasSize_1
[decl #25600] theorem List.modifyTailIdx_id
[decl #25700] theorem Vector.one_le_countP_iff
[decl #25800] theorem Option.max_pfilter_right
[decl #25900] theorem Lean.Grind.Nat.le_of_eq_1
[decl #26000] theorem List.max?_eq_some_iff
[decl #26100] theorem _private.Init.Data.BitVec.Lemmas.0.BitVec.getLsbD_true_of_eq_clzAuxRec_of_ne_zero._proof_1_2
[decl #26200] theorem _private.Init.Data.Range.Polymorphic.NatLemmas.0.Nat.getElem!_toArray_rco_eq_zero_iff._simp_1_2
[decl #26300] def IO.asTask
[decl #26400] theorem Option.foldr_toList
[decl #26500] theorem Int.ediv_le_self
[decl #26600] theorem Lean.Grind.CutsatConfig.mk.inj
[decl #26700] def Sum.instDecidableLiftRel.match_1
[decl #26800] theorem Int64.zero_add
[decl #26900] theorem _private.Init.Data.List.Nat.Erase.0.List.eraseIdx_set_lt._proof_1_2
[decl #27000] def Std.PRange.UpwardEnumerable.ctorIdx
[decl #27100] theorem Array.mapFinIdx_congr
[decl #27200] def Int64.decLt
[decl #27300] theorem Std.IterM.toList_flatMapAfterM
[decl #27400] def instInhabitedForInStep.default
[decl #27500] theorem ListSlice.toList_mkSlice_ric
[decl #27600] theorem String.Slice.Pos.Splits.exists_eq_append_singleton_of_ne_startPos
[decl #27700] theorem Int.toArray_rco_eq_singleton_append_iff
[decl #27800] theorem ISize.ofInt_tdiv
[decl #27900] theorem Nat.mul_ne_mul_left
[decl #28000] theorem Array.le_antisymm
[decl #28100] theorem _private.Init.Data.BitVec.Bitblast.0.BitVec.bit_neg_eq_neg._simp_1_1
[decl #28200] def Inter.noConfusion
[decl #28300] def String.Slice.ctorIdx
[decl #28400] def BitVec.getElem_sdiv.match_1
[decl #28500] def Subsingleton.recOn
[decl #28600] def Substring.Raw.repair
[decl #28700] theorem Nat.gcd_mul_gcd_of_coprime_of_mul_eq_mul
[decl #28800] theorem Nat.lcm_dvd_mul_self_left_iff_dvd_mul
[decl #28900] theorem Nat.mul_div_le_mul_div_assoc
[decl #29000] def Substring.Raw.isEmpty
[decl #29100] theorem Fin.cast_natAdd_left
[decl #29200] theorem _private.Init.Data.List.Nat.Range.0.List.erase_range'._proof_1_8
[decl #29300] def Lean.Meta.Simp.Config.iota
[decl #29400] theorem Int64.toInt16_mul
[decl #29500] theorem Std.Rio.mem_iff
[decl #29600] theorem Nat.length_toList_rio
[decl #29700] theorem _private.Init.Data.String.Slice.0.String.Slice.takeWhile.go._proof_1
[decl #29800] theorem List.filterMap_map
[decl #29900] theorem ISize.toInt_ofBitVec
[decl #30000] theorem String.toList.eq_1
[decl #30100] theorem Std.instTotalLeOfLawfulOrderOrd
[decl #30200] theorem Int64.toInt8_and
[decl #30300] theorem Option.any_map
[decl #30400] def _private.Init.Data.Repr.0.Prod.reprTuple.match_1
[decl #30500] def WellFounded.casesOn
[decl #30600] theorem _private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rii.mem_toArray._simp_1_1
[decl #30700] theorem Vector.get_find?_replicate
[decl #30800] theorem Int16.instLawfulOrderOrd
[decl #30900] def Function.HasLeftInverse
[decl #31000] theorem ISize.left_eq_add
[decl #31100] theorem Nat.instCommutativeHOr
[decl #31200] def _private.Init.Data.String.Lemmas.Pattern.Split.0.String.Slice.Pattern.Model.SplitIterator.toList_eq_splitFromSteps.match_1_3
[decl #31300] theorem Vector.attach_map_subtype_val
[decl #31400] theorem _private.Init.Data.Range.Polymorphic.NatLemmas.0.Nat.zero_lt_getElem!_toArray_roc_iff._simp_1_1
[decl #31500] theorem Lean.Grind.smul_nat_eq_mul
[decl #31600] theorem _private.Init.Data.SInt.Lemmas.0.Int64.lt_or_lt_of_ne._simp_1_2
[decl #31700] theorem UInt8.toUInt32_neg
[decl #31800] def term_⊃_
[decl #31900] theorem Int.eq_mul_of_fdiv_eq_right
[decl #32000] theorem Int.Linear.norm_eq_cert.eq_1
[decl #32100] theorem Array.foldrM_reverse
[decl #32200] theorem Int64.instRxiHasSize.eq_1
[decl #32300] theorem Vector.le_toArray
[decl #32400] theorem _private.Init.Data.SInt.Bitwise.0.Int16.shiftRight_zero._simp_1_1
[decl #32500] theorem _private.Init.Data.Array.Range.0.Array.mem_zipIdx'._proof_1
[decl #32600] def term#[_,]
[decl #32700] theorem Option.pfilter_eq_pbind_ite
[decl #32800] theorem String.Slice.Pattern.Model.LawfulForwardPatternModel.dropPrefix?_eq_none_iff
REJECT: [String.Slice.Pattern.Model.LawfulToForwardSearcherModel.defaultImplementation] application argument type mismatch

Test "init-prelude"

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

Test result: 👍 accepted · exit code 0 · wall time: 141 ms · instructions: 1.1 G · max rss memory: 75.1 MB

stderr:

[decl #100] def Eq.casesOn
[decl #200] def Fin.Internal.ofNat
[decl #300] def Dvd.casesOn
[decl #400] theorem decide_eq_false
[decl #500] def EStateM.bind.match_1
[decl #600] def Lean.ParserDescr.noConfusion
[decl #700] def Lean.Name.mkSimple
[decl #800] def MonadExceptOf.tryCatch
[decl #900] def HAnd.hAnd
[decl #1000] def One.ctorIdx
[decl #1100] def Except.ctorIdx
[decl #1200] def OrElse.orElse
[decl #1300] theorem congrFun'
[decl #1400] def Bind.noConfusion
[decl #1500] def ShiftRight.noConfusion
[decl #1600] def Hashable.noConfusionType

Test "k-rec-conv"

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

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

stderr:

REJECT: [bad] theorem 61: value type does not match declared type

Test "large-elim-param"

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

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

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

stderr:

REJECT: [cast] def 9: value type does not match declared type

Test "large-elim-prop-bool"

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

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

Test "level-imax-leq"

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

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

stderr:

REJECT: [down] def 11: value type does not match declared type

Test "level-imax-normalization"

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

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

stderr:

REJECT: [down] def 11: value type does not match declared type

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

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

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

Test "mathlib"

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

Test result: ✋ rejected · exit code 1 · wall time: 3.1 m · instructions: 1.6 T · max rss memory: 11.1 GB

stderr:

[decl #100] def _private.Init.Prelude.0.Nat.ble_eq_true_of_le.match_1_4
[decl #200] def List.utf8Encode
[decl #300] def AddZero.toAdd
[decl #400] theorem List.mem_cons_self
[decl #500] def instHasEquivOfSetoid
[decl #600] def _private.Init.Data.Nat.Basic.0.Nat.succ_add.match_1_1
[decl #700] theorem instDecidableIff._proof_2
[decl #800] theorem decide_false
[decl #900] def Finset.instEmptyCollection
[decl #1000] theorem List.nodup_singleton
[decl #1100] theorem _private.Init.Data.List.Erase.0.List.erase_of_not_mem._simp_1_3
[decl #1200] theorem instNonemptyOfInhabited
[decl #1300] def _private.Init.Data.List.Perm.0.List.perm_append_comm.match_1_1
[decl #1400] def Inter.inter
[decl #1500] def Multiset.union
[decl #1600] theorem WellFounded.Nat.eager_eq
[decl #1700] def Int.mul
[decl #1800] theorem Int.add_left_cancel
[decl #1900] theorem Lean.Omega.IntList.mul_nil_right
[decl #2000] theorem Nat.mod_add_div
[decl #2100] theorem Int.neg_ediv_of_dvd
[decl #2200] theorem Lean.Omega.Coeffs.dot_smul_left
[decl #2300] def List.instGetElem?NatLtLength
[decl #2400] theorem Multiset.countP_add
[decl #2500] def Lean.Data.AC.Context.arbitrary
[decl #2600] def Int.Linear.Poly.add.noConfusion
[decl #2700] theorem List.filter_cons
[decl #2800] theorem Multiset.le_filter
[decl #2900] def _private.Init.PropLemmas.0.not_imp_of_and_not.match_1_1
[decl #3000] theorem _private.Init.PropLemmas.0.exists_eq_or_imp._simp_1_2
[decl #3100] theorem Finsupp.zipWith_apply
[decl #3200] def AddSubmonoid.toAddSubsemigroup
[decl #3300] def BoundedOrder.toOrderTop
[decl #3400] theorem Std.le_refl
[decl #3500] theorem Std.IsPreorder.le_refl
[decl #3600] def _private.Mathlib.Order.SetNotation.0.Set.mem_iUnion.match_1_3
[decl #3700] theorem Set.Subset.antisymm_iff
[decl #3800] theorem AddMonoidAlgebra.nonAssocSemiring._proof_2
[decl #3900] theorem AddMonoidAlgebra.singleZeroRingHom._proof_2
[decl #4000] theorem Monoid.toMulAction._proof_2
[decl #4100] def _private.Mathlib.Data.Finsupp.Defs.0.Finsupp.ext_iff'.match_1_1
[decl #4200] theorem Int.Linear.norm_le
[decl #4300] def Nat.Linear.Poly
[decl #4400] def Lean.Grind.CommRing.Mon.revlex
[decl #4500] theorem Lean.Grind.CommRing.Poly.beq'_eq
[decl #4600] theorem Int.eq_natAbs_of_nonneg
[decl #4700] theorem Lean.Grind.CommRing.Poly.mulMon.go.induct_unfolding
[decl #4800] theorem Lean.Grind.instCommRingInt._proof_5
[decl #4900] theorem List.find?_eq_none
[decl #5000] def Function.onFun
[decl #5100] theorem List.eq_nil_iff_forall_not_mem
[decl #5200] theorem Ideal.mul_mem_left
[decl #5300] theorem AddMonoidAlgebra.addAddCommGroup._proof_9
[decl #5400] theorem RingHom.comp_apply
[decl #5500] def SubMulAction.casesOn
[decl #5600] theorem _private.Mathlib.Data.Set.Image.0.Set.image_mono._proof_1_1
[decl #5700] theorem WithBot.instPreorder._proof_1
[decl #5800] theorem AddAction.mem_orbit_self
[decl #5900] def AddSubgroup.toAddGroup
[decl #6000] def QuotientAddGroup.Quotient.addGroup._aux_4
[decl #6100] theorem MulZeroClass.negZeroClass._proof_1
[decl #6200] def RingCon.instZeroQuotient._aux_1
[decl #6300] def RingCon.instSubQuotient._aux_1
[decl #6400] theorem AddSubgroup.orderIsoAddCon._proof_1
[decl #6500] theorem Function.Injective.mulOneClass._proof_2
[decl #6600] theorem Polynomial.finset_sum_coeff
[decl #6700] theorem Finset.le_sup
[decl #6800] def Units.inv
[decl #6900] def Units.map
[decl #7000] def CategoryTheory.Limits.MultispanIndex.fst
[decl #7100] theorem Mathlib.Tactic.Reassoc.eq_whisker'._to_dual_1
[decl #7200] theorem map_smul
[decl #7300] theorem Submonoid.instSubmonoidClass
[decl #7400] theorem Nat.gcd_one_left
[decl #7500] theorem DivisionSemiring.mul_inv_cancel
[decl #7600] theorem eq_or_lt_of_le
[decl #7700] theorem Commute.mul_self_eq_mul_self_iff
[decl #7800] theorem _private.Mathlib.Algebra.GroupWithZero.Defs.0.noZeroDivisors_iff_eq_zero_of_mul._simp_1_2
[decl #7900] theorem Units.mk0_val
[decl #8000] theorem Pi.nonAssocSemiring._proof_4
[decl #8100] theorem Nat.gcd_pos_of_pos_left
[decl #8200] def _private.Init.Data.Int.DivMod.Bootstrap.0.Int.emod_lt_of_pos.match_1_1
[decl #8300] theorem Nat.gcd_ne_zero_left
[decl #8400] theorem Int.tdiv_mul_cancel_of_tmod_eq_zero
[decl #8500] theorem Int.one_ne_zero
[decl #8600] def instDecidableForall
[decl #8700] def Rat.commSemiring
[decl #8800] theorem nsmul_two_semiclosed
[decl #8900] theorem Int.cast_ofNat
[decl #9000] def Lean.Grind.CommRing.Stepwise.core_cert
[decl #9100] def Int._sizeOf_1
[decl #9200] theorem Nat.eq_zero_of_le_zero
[decl #9300] theorem Real.mk_le
[decl #9400] def Real.definition._@.Mathlib.Data.Real.Basic.1934218611._hygCtx._hyg.8
[decl #9500] def HeytingAlgebra.toBoundedOrder
[decl #9600] theorem List.getElem_cons
[decl #9700] def Fintype.ofFinset
[decl #9800] def List.pairwise_lt_range'._auto_1
[decl #9900] theorem NormedField.toNormedDivisionRing._proof_8
[decl #10000] theorem Filter.isGLB_sInf
[decl #10100] theorem GaloisConnection.l_sSup
[decl #10200] theorem Lean.Grind.AC.Seq.var.injEq
[decl #10300] def GaloisConnection.liftOrderBot
[decl #10400] theorem coinduced_le_iff_le_induced
[decl #10500] theorem Filter.mem_inf_of_inter
[decl #10600] theorem nhdsGE_eq_iInf_inf_principal
[decl #10700] theorem le_self_pow₀
[decl #10800] theorem Homeomorph.isInducing
[decl #10900] theorem Set.Nonempty.ne_empty
[decl #11000] theorem lt_inv_of_lt_inv₀
[decl #11100] theorem TwoSidedIdeal.rel_iff
[decl #11200] def NonUnitalSeminormedRing.toPseudoMetricSpace
[decl #11300] theorem CauSeq.Completion.Cauchy.ring._proof_38
[decl #11400] def NNRat.instDistribSMul
[decl #11500] theorem Real.commRing._proof_21
[decl #11600] theorem Real.ofCauchy_nnratCast
[decl #11700] def instZeroENNReal
[decl #11800] theorem WithTop.lattice._proof_3
[decl #11900] def Nonneg.semilatticeInf._aux_1
[decl #12000] theorem WithTop.instNonUnitalNonAssocSemiring._proof_4
[decl #12100] theorem ENNReal.coe_inj
[decl #12200] theorem isClosed_sInter
[decl #12300] theorem Filter.Tendsto.le_comap
[decl #12400] theorem _private.Mathlib.Order.Bounds.Basic.0.lt_isLUB_iff._simp_1_4
[decl #12500] theorem Int.floor_nonpos
[decl #12600] theorem Nat.commute_cast
[decl #12700] def Int.leastOfBdd.match_3
[decl #12800] theorem OrderIso.isLUB_image
[decl #12900] theorem Set.image_empty
[decl #13000] theorem WithTop.instCompleteLinearOrder._proof_9
[decl #13100] theorem NNReal.instSemifield._proof_12
[decl #13200] theorem CanonicallyOrderedAdd.toLinearOrderedCommGroupWithZero._proof_8
[decl #13300] theorem abs_sub_le
[decl #13400] theorem T1Space.t1
[decl #13500] theorem subset_interior_iff_mem_nhdsSet
[decl #13600] def Filter.GenerateSets.recOn
[decl #13700] theorem iSup_range
[decl #13800] def _private.Mathlib.Order.Directed.0.IsMax.isTop.match_1_1
[decl #13900] theorem Prod.pseudoEMetricSpaceMax._proof_4
[decl #14000] theorem dist_dist_dist_le
[decl #14100] theorem Real.normedField._proof_14
[decl #14200] def _private.Mathlib.Tactic.NormNum.Result.0.Mathlib.Meta.NormNum.IsInt.to_raw_eq.match_1_1
[decl #14300] theorem isPreconnected_closed_iff
[decl #14400] theorem instPseudoMetricSpaceNNReal._proof_8
[decl #14500] theorem NNReal.powOrderIso._proof_3
[decl #14600] theorem Complex.normSq_zero
[decl #14700] theorem Lean.Grind.CommRing.Stepwise.d_init
[decl #14800] theorem IsCauSeq.of_abv
[decl #14900] theorem div_self
[decl #15000] theorem Nat.cast_pow
[decl #15100] theorem Finset.sum_nonneg
[decl #15200] theorem NNRat.instSemifield._proof_4
[decl #15300] theorem Nat.choose_succ_succ
[decl #15400] def Finset.Icc
[decl #15500] theorem uniformContinuous_sub
[decl #15600] def EMetricSpace.toPseudoEMetricSpace
[decl #15700] theorem _private.Mathlib.Topology.Separation.Basic.0.t0Space_iff_not_inseparable._simp_1_1
[decl #15800] theorem MulAction.compHom._proof_2
[decl #15900] theorem Set.fintypeLENat._proof_1
[decl #16000] theorem _private.Mathlib.Topology.UniformSpace.Real.0.Real.instCompleteSpace._simp_1
[decl #16100] theorem add_lt_add_of_lt_of_le
[decl #16200] theorem IsUnit.div_eq_iff
[decl #16300] theorem zero_lt_three
[decl #16400] theorem OrderDual.instAddCommGroup._proof_1
[decl #16500] theorem Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq
[decl #16600] theorem Complex.cosh_conj
[decl #16700] theorem Function.leftInverse_surjInv
[decl #16800] theorem Real.abs_sin_le_one
[decl #16900] theorem MulOpposite.instMulOneClass._proof_2
[decl #17000] theorem _private.Mathlib.Topology.UniformSpace.UniformEmbedding.0.isComplete_image_iff._simp_1_3
[decl #17100] theorem SemilinearEquivClass.toAddEquivClass
[decl #17200] theorem _private.Mathlib.Order.Filter.IsBounded.0.OrderIso.isBoundedUnder_le_comp._simp_1_1
[decl #17300] theorem Subtype.coe_mk
[decl #17400] theorem Complex.IsExpCmpFilter.isTheta_cpow_exp_re_mul_log
[decl #17500] def Pi.subtractionMonoid
[decl #17600] theorem Asymptotics.IsBigOWith.comp_tendsto
[decl #17700] theorem Set.ordConnectedProj._proof_1
[decl #17800] theorem Set.compl_ordConnectedSection_ordSeparatingSet_mem_nhdsLE
[decl #17900] theorem Set.iUnion_of_empty
[decl #18000] theorem SubgroupClass.toInvMemClass
[decl #18100] def Std.DTreeMap.Internal.Impl.balanceLErase.match_5
[decl #18200] theorem _private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balance!_eq_balanceₘ._proof_1_15
[decl #18300] theorem Std.DTreeMap.Internal.Impl.balanced_balanceL._simp_1
[decl #18400] theorem Std.DTreeMap.Internal.Impl.erase._proof_7
[decl #18500] theorem _private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.size_glue._proof_1_11
[decl #18600] theorem _private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.Const.alter._proof_28
[decl #18700] theorem _private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.filter._proof_3
[decl #18800] theorem Std.DTreeMap.Equiv.trans
[decl #18900] theorem Std.DTreeMap.Internal.Impl.applyPartition.eq_1
[decl #19000] theorem Std.DTreeMap.Internal.Impl.toListModel_filter_lt_of_lt
[decl #19100] theorem _private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.updateCell._proof_62
[decl #19200] theorem Std.DTreeMap.Internal.Impl.modify.eq_2
[decl #19300] theorem Std.DTreeMap.Equiv.inner
[decl #19400] theorem Std.DTreeMap.Internal.Impl.getKey!_eq_getKey!ₘ
[decl #19500] theorem DirectLimit.instMonoid._proof_9
[decl #19600] def ByteArray.utf8Decode?.go.match_1
[decl #19700] def instHOrOfOrOp
[decl #19800] theorem Nat.testBit_two_pow_mul
[decl #19900] def UInt32.decLt._aux_1
[decl #20000] def ByteArray.utf8DecodeChar?
[decl #20100] theorem _private.Init.Data.String.Decode.0.Char.utf8Size_eq_three_iff._simp_1_3
[decl #20200] def _private.Init.GetElem.0.List.getElem_cons_drop.match_1_1
[decl #20300] theorem _private.Init.Data.String.Decode.0.String.utf8EncodeChar_eq_utf8EncodeCharFast._proof_1_13
[decl #20400] theorem _private.Init.Data.Array.Extract.0.Array.extract_append_extract._proof_1_3
[decl #20500] def _private.Init.Data.Nat.Lemmas.0.Nat.one_lt_two_pow.match_1_1
[decl #20600] theorem BitVec.cons_append
[decl #20700] theorem _private.Init.Data.String.Decode.0.Char.toNat_val_le._proof_1_1
[decl #20800] theorem _private.Init.Data.ByteArray.Lemmas.0.ByteArray.append_inj_left._simp_1_1
[decl #20900] def String.instOrd
[decl #21000] def _private.Init.Data.Nat.Basic.0.Nat.zero_lt_sub_of_lt.match_1_1
[decl #21100] def _private.Std.Data.DHashMap.Internal.Defs.0.Std.DHashMap.Internal.Raw₀.Const.modify.match_1
[decl #21200] def FloatSpec.float
[decl #21300] def Lean.Meta.SynthInstanceCacheKey.casesOn
[decl #21400] def Std.HashMap.instMembership
[decl #21500] def Lean.isIdFirst
[decl #21600] theorem String.Pos.Raw.isValid_empty_iff._simp_1
[decl #21700] theorem List.take_eq_take_min
[decl #21800] theorem Array.append_inj_left'
[decl #21900] def UInt8.instDecidableIsUTF8FirstByte
[decl #22000] def String.Slice.sliceTo
[decl #22100] def Std.Iter.IsPlausibleSuccessorOf
[decl #22200] theorem String.Pos.Raw.byteIdx_inc
[decl #22300] def Char.toLower
[decl #22400] theorem Std.Iterators.Types.FilterMap.instIterator._proof_5
[decl #22500] def ST.Ref.modifyGet
[decl #22600] def _private.Lean.Exception.0.Lean.Exception.hasSyntheticSorry.match_1
[decl #22700] theorem _private.Init.Data.Array.BinSearch.0.Array.binSearch._proof_3
[decl #22800] def _private.Lean.Meta.WHNF.0.Lean.Meta.matchConstAux.match_1
[decl #22900] def Lean.Level.updateIMax!
[decl #23000] def Array.set!
[decl #23100] def Lean.Meta.whnfD
[decl #23200] def Lean.LocalDecl.value?
[decl #23300] theorem InitialSeg.trans._proof_1
[decl #23400] def _private.Mathlib.Order.RelIso.Basic.0.RelEmbedding.trichotomous.match_1_1
[decl #23500] def _private.Init.Data.Sum.Basic.0.Sum.lex_inr_inl.match_1_1
[decl #23600] theorem LinearMap.module._proof_1
[decl #23700] theorem instDiscreteTopologyBool
[decl #23800] def Profinite.NobelingProof.GoodProducts.sum_to
[decl #23900] theorem List.prod_eq_zero_iff
[decl #24000] theorem _private.Mathlib.Topology.Category.Profinite.Nobeling.Basic.0.Profinite.NobelingProof.Products.eval_πs._simp_1_1
[decl #24100] theorem List.IsChain.sortedGT
[decl #24200] def MulOpposite.instInv
[decl #24300] theorem FreeGroup.instGroup._proof_8
[decl #24400] def Subgroup.normalClosure
[decl #24500] theorem Multiplicative.monoid._proof_1
[decl #24600] def Abelianization.of
[decl #24700] theorem Multiset.singleton_ne_zero
[decl #24800] def TensorProduct.addCommSemigroup
[decl #24900] theorem LinearMap.llcomp._proof_1
[decl #25000] theorem Std.DHashMap.Internal.Raw.get_eq._proof_2
[decl #25100] theorem instLawfulHashableOfLawfulBEq
[decl #25200] theorem List.Perm.of_eq
[decl #25300] theorem List.Sublist.map
[decl #25400] theorem _private.Std.Data.Internal.List.Associative.0.Std.Internal.List.length_alterKey._simp_1_4
[decl #25500] theorem _private.Std.Data.Internal.List.Associative.0.Std.Internal.List.getValueCast_mem._simp_1_5
[decl #25600] theorem LinearMap.ext_iff
[decl #25700] def _private.Mathlib.Logic.Function.Basic.0.Function.bijective_iff_has_inverse.match_1_1
[decl #25800] theorem _private.Mathlib.Order.Preorder.Chain.0.IsChain.superChain_succChain._simp_1_2
[decl #25900] def Multiset.chooseX
[decl #26000] theorem Set.subset_iInter_iff._simp_1
[decl #26100] theorem _private.Mathlib.Data.Finsupp.Single.0.Finsupp.single_eq_zero._simp_1_1
[decl #26200] theorem LinearIndependent.linearCombination_repr
[decl #26300] theorem Submodule.gi._proof_1
[decl #26400] theorem iSup_le_iff
[decl #26500] def Cardinal.instZero
[decl #26600] theorem nonempty_unique
[decl #26700] def Cardinal.aleph0
[decl #26800] theorem Finset.sum_pi_single
[decl #26900] theorem Fintype.card_coe
[decl #27000] theorem Equiv.nonempty
[decl #27100] theorem Infinite.of_cardinalMk_le
[decl #27200] theorem Sigma.mk.inj_iff
[decl #27300] theorem RelIso.sumLexComplLeft._proof_1
[decl #27400] theorem Ordinal.lt_lift_iff
[decl #27500] theorem WCovBy.ge_of_gt
[decl #27600] theorem Ordinal.isInitial_ord
[decl #27700] theorem Finset.not_nonempty_empty
[decl #27800] theorem Ordinal.one_ne_zero
[decl #27900] theorem Infinite.false
[decl #28000] def Equiv.add
[decl #28100] theorem Module.addCommMonoidToAddCommGroup._proof_1
[decl #28200] theorem AddSubmonoid.subtype._proof_1
[decl #28300] theorem Finset.image_empty
[decl #28400] def _private.Mathlib.Data.Set.Insert.0.Set.eq_singleton_iff_nonempty_unique_mem.match_1_1
[decl #28500] theorem LinearMap.iterateMapComap_eq_succ
[decl #28600] theorem Subsemiring.toSemiring._proof_6
[decl #28700] theorem MvPolynomial.eval₂Hom_X'
[decl #28800] theorem Fin.subNat._proof_1
[decl #28900] theorem Polynomial.algHom_ext'
[decl #29000] theorem WithBot.add_bot
[decl #29100] theorem Lean.Grind.Ring.OfSemiring.Q.exact
[decl #29200] def Subalgebra.copy
[decl #29300] theorem AddSubgroup.mem_sInf
[decl #29400] theorem RingHom.mem_range
[decl #29500] theorem DFinsupp.distribMulAction._proof_2
[decl #29600] theorem rank_finsupp
[decl #29700] theorem SubfieldClass.toDivisionRing._proof_25
[decl #29800] theorem Lean.Grind.IntInterval.mem_io._simp_1
[decl #29900] theorem Lean.Grind.Fin.instCommRingFinOfNeZeroNat._proof_8
[decl #30000] def MulOpposite.instAddCommMonoid
[decl #30100] theorem MulOpposite.instDivisionSemiring._proof_6
[decl #30200] def Finsupp.sigmaFinsuppAddEquivPiFinsupp
[decl #30300] theorem LinearMap.coe_comp
[decl #30400] theorem ENat.coe_ne_top
[decl #30500] theorem Module.Basis.toDual_linearCombination_left
[decl #30600] def Function.Injective.nonUnitalNonAssocRing
[decl #30700] def Equiv.swapCore
[decl #30800] theorem MonoidHom.map_isConj
[decl #30900] theorem Finset.sum_mul_sum
[decl #31000] theorem Pi.instFintype._proof_1
[decl #31100] theorem Matrix.one_apply_eq
[decl #31200] def AddMonoid.End.instAddCommMonoid
[decl #31300] theorem Matrix.detp_smul_adjp
[decl #31400] theorem AlternatingMap.instSMul._proof_1
[decl #31500] theorem Pi.disjoint_iff
[decl #31600] theorem List.instDecidablePairwise._proof_3
[decl #31700] def Pi.ringHom
[decl #31800] theorem IsField.mul_comm
[decl #31900] theorem AddSubgroup.mem_mk
[decl #32000] theorem Module.Basis.coe_extend
[decl #32100] theorem Module.instIsReflexiveOfFiniteOfProjective
REJECT: [_private.Mathlib.LinearAlgebra.PerfectPairing.Restrict.0.LinearMap.restrictScalars_field_aux] application argument type mismatch

Test "nat-rec-k-lie"

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

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

stderr:

REJECT: [k1] theorem 29: value type does not match declared type

Test "nat-rec-rules"

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

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

stderr:

REJECT: [proof_of_false] application argument type mismatch

Test "nested-nonuniform-param"

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

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

stderr:

REJECT: [E] non-uniform nested inductive parameter

Test "nested-unused-param"

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

Test result: ✋ rejected · exit code 1 · wall time: 8 ms · instructions: 14.8 M · max rss memory: 10.9 MB

stderr:

REJECT: [E] projection struct name mismatch

Test "orphan-ctor"

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

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

Test "orphan-rec"

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

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

stderr:

REJECT: recursor `rogue` is not named `I.rec` for an inductive in this group

Test "perf/app-lam"

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

Test result: 👍 accepted · exit code 0 · wall time: 56 ms · instructions: 332.1 M · max rss memory: 179.4 MB

Test "perf/args-before-unfold"

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

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

Test result: 👍 accepted · exit code 0 · wall time: 10 ms · instructions: 31.4 M · max rss memory: 13.9 MB

Test "perf/beta-ladder"

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

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

Test result: 👍 accepted · exit code 0 · wall time: 1.4 s · instructions: 4.0 G · max rss memory: 840.5 MB

Test "perf/church-numerals"

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

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

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

stderr:

REJECT: [kernel_church_numerals] theorem 20: value type does not match declared type

Test "perf/discarded-argument"

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

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

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

Test "perf/discarded-argument-match"

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

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

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

Test "perf/folded-constant-first"

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

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

Test result: 👍 accepted · exit code 0 · wall time: 10 ms · instructions: 39.4 M · max rss memory: 13.5 MB

Test "perf/folded-constant-last"

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

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

Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 39.3 M · max rss memory: 13.5 MB

Test "perf/grind-ring-5"

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

Test result: 👍 accepted · exit code 0 · wall time: 3.4 s · instructions: 26.1 G · max rss memory: 505.7 MB

stderr:

[decl #100] theorem Nat.succ_le_succ
[decl #200] def List.utf8Encode
[decl #300] def Exists.casesOn
[decl #400] theorem Lean.Grind.AddCommGroup.neg_add_cancel
[decl #500] theorem Nat.add_sub_cancel_left
[decl #600] theorem Int.nonneg_or_nonneg_neg
[decl #700] def Lean.Omega.Constraint.sat
[decl #800] def Int.instDiv
[decl #900] theorem WellFounded.Nat.fix_eq
[decl #1000] theorem Int.negSucc_eq
[decl #1100] def _private.Init.Data.Int.DivMod.Bootstrap.0.Int.emod_emod_of_dvd.match_1_1
[decl #1200] def GetElem?.getElem?
[decl #1300] theorem Nat.lt_or_gt_of_ne
[decl #1400] theorem Bool.false_eq_true
[decl #1500] theorem Int.add_le_add_iff_right._simp_1
[decl #1600] def Prod.lex
[decl #1700] def Bool.dcond.match_1
[decl #1800] theorem Lean.Grind.CommRing.instBEqMon.beq.eq_3
[decl #1900] theorem Lean.Grind.Semiring.ofNat_mul
[decl #2000] theorem Lean.Grind.CommRing.denoteInt_eq

Test "perf/identical-nesting"

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

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

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

Test "perf/irrelevance-before-evaluation"

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

slowTriv (count #n) = True.intro

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

Test "perf/let-ladder"

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

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

Test result: 👍 accepted · exit code 0 · wall time: 1.4 s · instructions: 4.2 G · max rss memory: 838.6 MB

Test "perf/refute-cheap-first"

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

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

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

stderr:

REJECT: [kernel_refute_cheap_first] theorem 57: value type does not match declared type

Test "perf/refute-cheap-last"

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

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

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

stderr:

REJECT: [kernel_refute_cheap_last] theorem 57: value type does not match declared type

Test "perf/repeated-subproblem"

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

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

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

Test "perf/shared-subterm"

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

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

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

Test "perf/shift-cascade"

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

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

Test "perf/unroll-versus-evaluate"

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

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

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 38.7 M · max rss memory: 13.3 MB

Test "proj-non-structure"

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

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

stderr:

REJECT: [bad] projection: not a single-constructor inductive

Test "proj-of-imax-prop"

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

Test result: ✋ rejected · exit code 1 · wall time: 8 ms · instructions: 6.2 M · max rss memory: 8.8 MB

stderr:

REJECT: [imaxProjBool] cannot project a Type field from a Prop structure

Test "proj-of-prop"

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

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

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

stderr:

REJECT: [badFalse] application argument type mismatch

Test "proj-of-stuck-prop"

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

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

stderr:

REJECT: [Native64ResultSortOwner] expected a sort

Test "proj-of-subst-prop"

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

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

stderr:

REJECT: [PR14806Subst.Owner] expected a sort

Test "proof-irrel"

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

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

Test "rec-k-lie"

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

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

stderr:

REJECT: [bad] theorem 30: value type does not match declared type

Test "rec-missing-ih"

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

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

stderr:

REJECT: [Native64TwoHashOwner] occurrence of inductive type in unsupported position

Test "rec-of-subst-prop"

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

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

stderr:

REJECT: [Issue.Owner] expected a sort

Test "sparse-name-index"

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

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

Test "std"

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

Test result: 💥 error · exit code 137 · wall time: 19.0 m · instructions: 8.3 T · max rss memory: 14.2 GB

stderr:

[decl #100] def WellFounded.Nat.fix
[decl #200] theorem eq_true
[decl #300] def Nat.testBit
[decl #400] theorem Nat.div_add_mod
[decl #500] theorem Nat.zero_lt_succ._simp_1
[decl #600] def Nat.Linear.Expr.toPoly.go
[decl #700] theorem Nat.testBit_bitwise
[decl #800] def Int.casesOn
[decl #900] theorem _private.Init.Data.Int.Lemmas.0.Int.add_assoc.aux2
[decl #1000] theorem Int.max_comm
[decl #1100] def Nat.toDigits
[decl #1200] theorem Lean.Omega.IntList.mul_neg_left
[decl #1300] def Lean.Omega.tidy?.match_1
[decl #1400] def _private.Init.Data.Nat.Basic.0.Nat.sub_le_sub_left.match_1_1
[decl #1500] def _private.Init.Data.Nat.Dvd.0.Nat.dvd_antisymm.match_1_1
[decl #1600] theorem Int.neg_neg_of_pos
[decl #1700] def Pure.pure
[decl #1800] def LawfulMonad.mk'._auto_5
[decl #1900] def Std.HashMap.Raw.getKey
[decl #2000] theorem List.getElem_drop._proof_1
[decl #2100] def _private.Init.PropLemmas.0.exists_or.match_1_1
[decl #2200] theorem Std.Internal.List.keys_eq_map
[decl #2300] theorem Std.DHashMap.Internal.AssocList.foldl_eq
[decl #2400] def Option.get.match_1
[decl #2500] theorem List.exists_of_eraseP
[decl #2600] theorem List.foldl_cons
[decl #2700] theorem Std.Internal.List.mem_eraseKey_of_key_ne
[decl #2800] theorem _private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Const.length_alterKey._simp_1_4
[decl #2900] def Std.DTreeMap.Internal.Impl.size
[decl #3000] theorem Std.DTreeMap.Internal.Impl.balanceL.match_5.congr_eq_2
[decl #3100] theorem _private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balance!_eq_balanceₘ._simp_1_8
[decl #3200] def Lean.Data.AC.EvalInformation.evalVar
[decl #3300] theorem _private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanced_rotateR._proof_1_3
[decl #3400] theorem _private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.link._proof_5
[decl #3500] def Std.DTreeMap.Internal.Impl.glue
[decl #3600] def Std.DTreeMap.Internal.Impl.Const.alter.match_1
[decl #3700] theorem Std.DTreeMap.Internal.Impl.link2._unary._proof_2
[decl #3800] theorem Std.DTreeMap.Internal.Impl.Const.mergeWith._proof_1
[decl #3900] def _private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.insertMin.match_3.splitter
[decl #4000] def List.min
[decl #4100] def Std.Tactic.BVDecide.BVBit.noConfusionType
[decl #4200] theorem Std.Tactic.BVDecide.BVExpr.const.injEq
[decl #4300] theorem Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq._proof_31
[decl #4400] theorem Std.Tactic.BVDecide.BVExpr.decEq._proof_149
[decl #4500] def Std.DTreeMap.Internal.Impl.minKey
[decl #4600] theorem _private.Init.Data.List.Find.0.List.find?_eq_some_iff_append._simp_1_3
[decl #4700] theorem _private.Init.Data.List.Lemmas.0.List.filter_eq_nil_iff._simp_1_2
[decl #4800] theorem _private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.updateCell._proof_48
[decl #4900] theorem forall_eq'._simp_1
[decl #5000] theorem Std.Internal.List.isSome_minEntry?_eq_not_isEmpty
[decl #5100] def _private.Init.PropLemmas.0.Exists.imp.match_1_1
[decl #5200] def Std.Do.ExceptConds.entails.match_1
[decl #5300] theorem Std.DTreeMap.Internal.Impl.minKeyD.induct_unfolding
[decl #5400] theorem Std.DTreeMap.Internal.Impl.getKey!_eq_getKey!ₘ
[decl #5500] def Lean.Grind.CommRing.Var
[decl #5600] theorem forall_self_imp
[decl #5700] def String.Slice.startInclusive
[decl #5800] theorem List.reverse_reverse
[decl #5900] def UInt32.ofNatLT
[decl #6000] theorem _private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.parseFirstByte_eq_done_iff_toBitVec._simp_1_1
[decl #6100] theorem Nat.lt_or_eq_of_le
[decl #6200] def UInt32.land
[decl #6300] theorem _private.Init.Data.String.Decode.0.parseFirstByte_eq_done_of_utf8DecodeChar?_eq_some._proof_1_5
[decl #6400] theorem _private.Init.Data.BitVec.Lemmas.0.BitVec.extractLsb'_append_eq_ite._proof_1_5
[decl #6500] theorem _private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.toBitVec_eq_of_parseFirstByte_eq_oneMore
[decl #6600] theorem BitVec.cons._proof_1
[decl #6700] theorem _private.Init.Data.ByteArray.Lemmas.0.ByteArray.extract_add_four._proof_1_1
[decl #6800] theorem ByteArray.utf8Decode?.go._unary.eq_def
[decl #6900] theorem List.utf8Encode_eq_empty._simp_1
[decl #7000] def _private.Init.Data.String.Decode.0.UInt8.isUTF8FirstByte_getElem_utf8EncodeChar.match_1_2
[decl #7100] theorem Std.DHashMap.Internal.AssocList.get!_eq
[decl #7200] theorem Std.Sat.AIG.instLawfulOperatorBinaryInputMkGateCached
[decl #7300] def Std.Sat.Literal.negate
[decl #7400] theorem Std.DHashMap.distinct_keys
[decl #7500] theorem Lean.Grind.eq_congr
[decl #7600] def Int.sign.match_1
[decl #7700] def Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRightConst.go._unary
[decl #7800] theorem Lean.Grind.Ring.intCast_natCast_add_one
[decl #7900] def Std.DTreeMap.Internal.Impl.insertIfNew!
[decl #8000] theorem Std.Internal.List.insertEntryIfNew_of_perm
[decl #8100] theorem Array.mapFinIdx_induction
[decl #8200] theorem _private.Std.Sat.AIG.RefVecOperator.Zip.0.PSigma.casesOn._arg_pusher
[decl #8300] def Std.Tactic.BVDecide.BoolExpr.eval
[decl #8400] def Int.recOn
[decl #8500] def DecidableLE
[decl #8600] def Std.Iter.step
[decl #8700] theorem Std.IterStep.yield.inj
[decl #8800] def Int8.instNeg
[decl #8900] theorem BitVec.le_total
[decl #9000] theorem BitVec.add_neg_eq_sub
[decl #9100] def _private.Init.Data.Int.DivMod.Lemmas.0.Int.emod_lt.match_1_1
[decl #9200] theorem _private.Init.Data.Range.Polymorphic.SInt.0.HasModel.toNat_toInt_add_one_sub_toInt
[decl #9300] theorem Int8.eq_iff_toBitVec_eq
[decl #9400] theorem Std.DHashMap.Internal.Raw₀.interSmallerFn_eq_interSmallerFnₘ
[decl #9500] def Std.DTreeMap.Internal.Cell.Const.get?.match_1
[decl #9600] theorem Array.forIn'.loop._proof_2
[decl #9700] theorem Fin.mul_comm
[decl #9800] theorem _private.Init.Data.List.ToArray.0.List.findFinIdx?_loop_toArray._proof_1_2
[decl #9900] theorem _private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.getEntryGT?_eq_find?._simp_1_1
[decl #10000] def Std.ExtHashSet.inner
[decl #10100] def Std.Rxc.instIteratorIteratorIdOfUpwardEnumerableOfDecidableLE
[decl #10200] theorem USize.decEq._proof_1
[decl #10300] def Std.Iterators.Types.FilterMap.instIterator
[decl #10400] def Std.DTreeMap.Internal.Impl.entryAtIdx?.match_1
[decl #10500] theorem Std.DTreeMap.Internal.Impl.WF.filterMap
[decl #10600] theorem Std.Internal.Small.of_surjective
[decl #10700] theorem Std.Iterators.Types.ListIterator.instIterator._proof_1
[decl #10800] theorem _private.Init.Data.String.PosRaw.0.String.Pos.Raw.offsetBy_zero_left._simp_1_1
[decl #10900] theorem Nat.gcd_mul_left
[decl #11000] theorem _private.Std.Time.DateTime.PlainDateTime.0.Std.Time.PlainDateTime.ofTimestampAssumingUTC._proof_11
[decl #11100] def Std.Time.TimeZone.Offset.second
[decl #11200] theorem Int.ediv_one
[decl #11300] theorem Nat.mul_right_comm
[decl #11400] theorem String.Slice.Pos.isUTF8FirstByte_byte
[decl #11500] theorem _private.Init.Data.String.Defs.0.String.utf8ByteSize_eq_zero_iff._simp_1_2
[decl #11600] theorem Std.DHashMap.Internal.Raw₀.Const.toArray_toList_eq_toArray
[decl #11700] theorem List.getElem_mapFinIdx_go._proof_4
[decl #11800] theorem _private.Init.Data.Rat.Lemmas.0.Rat.nonneg_antisymm._proof_1_3
[decl #11900] def Std.Iterators.ULiftT
[decl #12000] def BitVec.sdiv_eq.match_1
[decl #12100] theorem _private.Init.Data.BitVec.Lemmas.0.BitVec.neg_eq_not_add._proof_1_1
[decl #12200] theorem BitVec.getMsbD_zero
[decl #12300] theorem Std.Internal.List.getValue_insertListConst_of_mem
[decl #12400] def Std.Time.Millisecond.Offset
[decl #12500] def _private.Std.Time.Date.Unit.Month.0.Std.Time.Month.Ordinal.cumulativeDays.match_1
[decl #12600] def String.join
[decl #12700] theorem _private.Init.Data.Array.Lemmas.0.Array.getElem_ofFn_go._proof_1_5
[decl #12800] theorem Std.DTreeMap.mem_union_of_left
[decl #12900] theorem Std.Sat.AIG.mkGate._proof_3
[decl #13000] theorem _private.Init.Data.String.Lemmas.FindPos.0.String.Slice.posGT_eq_next._simp_1
[decl #13100] theorem Std.LinearOrderPackage.ofLE._proof_2
[decl #13200] def WellFounded.extrinsicFix₃
[decl #13300] def Lean.Grind.CommRing.Expr.mul.elim
[decl #13400] theorem List.getElem?_reverse'
[decl #13500] theorem _private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Internal.Raw₀.insert_equiv_congr._simp_1_1
[decl #13600] def instAddISize
[decl #13700] def Std.Slice.Internal.ByteSliceData.casesOn
[decl #13800] theorem Vector.replicate_eq_mk_replicate
[decl #13900] theorem _private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rcc.length_toList._simp_1_5
[decl #14000] theorem UInt16.ofBitVec_uInt32ToBitVec
[decl #14100] def List.minOn
[decl #14200] theorem Std.Internal.List.getKeyD_insertList_of_contains_eq_false_right
[decl #14300] theorem Std.DTreeMap.mem_congr
[decl #14400] def Std.Internal.Parsec.instMonad
[decl #14500] def Std.Internal.Parsec.Input.next'
[decl #14600] theorem Int8.toInt_toInt64
[decl #14700] theorem Std.DHashMap.Const.get?_filterMap
[decl #14800] def Lean.Grind.CommRing.toRing
[decl #14900] def Std.Internal.IO.Process.ResourceUsageStats.mk.noConfusion
[decl #15000] def Std.Time.instHAddOffsetOffset_9
[decl #15100] def Std.DTreeMap.Internal.Impl.link2!._unary
[decl #15200] theorem WeaklyLawfulMonadAttach.map_attach
[decl #15300] theorem Vector.range'_one
[decl #15400] def instOrOpInt16
[decl #15500] theorem Nat.toList_rco_eq_cons_iff._simp_1
[decl #15600] def Lean.Grind.CommRing.Poly.denote'.go
[decl #15700] theorem Lean.Grind.CommRing.Mon.revlexWF.match_1.congr_eq_1
[decl #15800] def Lean.PrettyPrinter.Unexpander
[decl #15900] theorem Std.DTreeMap.mem_of_mem_insert
[decl #16000] def Std.DTreeMap.Const.unitOfList._auto_1
[decl #16100] def XorOp.noConfusionType
[decl #16200] theorem minOn_eq_right
[decl #16300] def Std.ExtTreeMap.getKeyD
[decl #16400] theorem List.not_of_lt_findIdx
[decl #16500] theorem _private.Init.Data.Nat.Fold.0.Nat.any_eq_anyTR._proof_1_2
[decl #16600] theorem Std.Internal.List.Const.maxKeyD_alterKey_eq_self
[decl #16700] theorem List.zipWith_toArray
[decl #16800] theorem _private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Internal.Raw₀.perm_keys_congr_left
[decl #16900] theorem _private.Std.Data.TreeMap.Lemmas.0.Std.TreeMap.equiv_iff_equiv
[decl #17000] theorem Std.Rxi.Iterator.Monadic.isPlausibleOutput_iff
[decl #17100] theorem Array.foldlM.loop.congr_simp
[decl #17200] def Std.DHashMap.Raw.filterMap
[decl #17300] theorem Std.Do.Spec.forIn'_rcc
[decl #17400] theorem Option.merge.eq_3
[decl #17500] theorem Std.Iterators.Types.ArrayIterator.instIterator._proof_1
[decl #17600] theorem _private.Std.Data.Iterators.Lemmas.Producers.Monadic.Array.0.Std.Iterators.Types.ArrayIterator.stepAsHetT_iterFromIdxM._simp_1_7
[decl #17700] theorem Lean.Grind.Linarith.instBEqPoly.beq_spec_2
[decl #17800] theorem ISize.not_lt
[decl #17900] theorem List.append_left_eq_self
[decl #18000] theorem Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBVBitBVVarBlastVar
[decl #18100] theorem _private.Std.Sat.AIG.If.0.Std.Sat.AIG.RefVec.ite._proof_3
[decl #18200] theorem Std.Sat.AIG.RefVec.fold_decl_eq
[decl #18300] def Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go
[decl #18400] theorem Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorShiftTargetBlastRotateRight
[decl #18500] def Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.go
[decl #18600] theorem Std.DHashMap.mem_insert_self
[decl #18700] theorem _private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Var.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go_denote_eq._proof_1_3

Test "tutorial/001_basicDef"

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

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

Test "tutorial/002_badDef"

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

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

stderr:

REJECT: [badDef] def 1: value type does not match declared type

Test "tutorial/003_arrowType"

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

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

Test "tutorial/004_dependentType"

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

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

Test "tutorial/005_constType"

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

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

Test "tutorial/006_betaReduction"

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

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

Test "tutorial/007_betaReduction2"

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

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

Test "tutorial/008_forallSortWhnf"

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

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

Test "tutorial/009_forallSortBad"

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

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

stderr:

REJECT: [forallSortBad] expected a sort

Test "tutorial/010_nonTypeType"

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

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

stderr:

REJECT: [nonTypeType] expected a sort

Test "tutorial/011_nonTypeAxiom"

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

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

stderr:

REJECT: [nonTypeAxiom] expected a sort

Test "tutorial/012_nonPropThm"

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

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

stderr:

REJECT: [nonPropThm] theorem 1: theorem type is not a Prop

Test "tutorial/013_levelComp1"

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

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

Test "tutorial/014_levelComp2"

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

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

Test "tutorial/015_levelComp3"

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

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

Test "tutorial/016_levelParams"

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

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

Test "tutorial/017_tut06_bad01"

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

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

stderr:

REJECT: [tut06_bad01] def 1: duplicate universe parameter

Test "tutorial/018_levelComp4"

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

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

Test "tutorial/019_levelComp5"

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

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

Test "tutorial/020_imax1"

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

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

Test "tutorial/021_imax2"

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

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

Test "tutorial/022_levelMaxComm"

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

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

Test "tutorial/023_levelMaxAssoc"

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

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

Test "tutorial/024_levelMaxIdem"

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

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

Test "tutorial/025_levelMaxAbsorb"

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

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

Test "tutorial/026_inferVar"

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

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

Test "tutorial/027_defEqLambda"

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

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

Test "tutorial/028_peano1"

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

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

Test "tutorial/029_peano2"

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

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

Test "tutorial/030_peano3"

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

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

Test "tutorial/031_letType"

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

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

Test "tutorial/032_letTypeDep"

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

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

Test "tutorial/033_letRed"

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

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

Test "tutorial/034_empty"

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

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

Test "tutorial/035_boolType"

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

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

Test "tutorial/036_twoBool"

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

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

Test "tutorial/037_andType"

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

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

Test "tutorial/038_prodType"

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

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

Test "tutorial/039_pprodType"

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

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

Test "tutorial/040_pUnitType"

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

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

Test "tutorial/041_eqType"

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

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

Test "tutorial/042_natDef"

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

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

Test "tutorial/043_rbTreeDef"

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

Test result: 👍 accepted · exit code 0 · wall time: 9 ms · instructions: 6.0 M · max rss memory: 8.8 MB

Test "tutorial/044_inductBadNonSort"

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

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

stderr:

REJECT: inductive `inductBadNonSort` is missing a recursor named `inductBadNonSort.rec`

Test "tutorial/045_inductBadNonSort2"

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

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

stderr:

REJECT: inductive `inductBadNonSort2` is missing a recursor named `inductBadNonSort2.rec`

Test "tutorial/046_inductLevelParam"

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

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

stderr:

REJECT: inductive `inductLevelParam` is missing a recursor named `inductLevelParam.rec`

Test "tutorial/047_inductTooFewParams"

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

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

stderr:

REJECT: inductive `inductTooFewParams` is missing a recursor named `inductTooFewParams.rec`

Test "tutorial/048_inductWrongCtorParams"

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

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

stderr:

REJECT: recursor `inductWrongCtorParams.rec` has numMotives=0 but group size is 1

Test "tutorial/049_inductWrongCtorResParams"

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

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

stderr:

REJECT: recursor `inductWrongCtorResParams.rec` has numMotives=0 but group size is 1

Test "tutorial/050_inductWrongCtorResLevel"

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

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

stderr:

REJECT: recursor `inductWrongCtorResLevel.rec` has numMotives=0 but group size is 1

Test "tutorial/051_inductInIndex"

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

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

stderr:

REJECT: recursor `inductInIndex.rec` has numMotives=0 but group size is 1

Test "tutorial/052_indNeg"

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

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

stderr:

REJECT: recursor `indNeg.rec` has numMotives=0 but group size is 1

Test "tutorial/053_reduceCtorParam.mk"

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

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

Test "tutorial/054_reduceCtorType.mk"

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

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

stderr:

REJECT: recursor `reduceCtorType.rec` has numMotives=0 but group size is 1

Test "tutorial/055_indNegReducible"

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

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

stderr:

REJECT: recursor `indNegReducible.rec` has numMotives=0 but group size is 1

Test "tutorial/056_predWithTypeField"

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

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

Test "tutorial/057_typeWithTypeField"

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

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

Test "tutorial/058_typeWithTypeFieldPoly"

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

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

Test "tutorial/059_typeWithTooHighTypeField.mk"

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

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

stderr:

REJECT: recursor `typeWithTooHighTypeField.rec` has numMotives=0 but group size is 1

Test "tutorial/060_emptyRec"

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

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

Test "tutorial/061_boolRec"

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

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

Test "tutorial/062_twoBoolRec"

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

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

Test "tutorial/063_andRec"

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

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

Test "tutorial/064_prodRec"

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

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

Test "tutorial/065_pprodRec"

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

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

Test "tutorial/066_punitRec"

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

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

Test "tutorial/067_eqRec"

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

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

Test "tutorial/068_nRec"

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

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

Test "tutorial/069_rbTreeRef"

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

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

Test "tutorial/070_boolPropRec"

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

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

Test "tutorial/071_BogusRecursor"

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

inductive BogusRecursor : Type where
  | mk : BogusRecursor

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

stderr:

REJECT: recursor `BogusRecursor.rec` has numMotives=0 but group size is 1

Test "tutorial/072_existsRec"

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

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

Test "tutorial/073_typeSingletonRecReduction"

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

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

Test "tutorial/074_sortElimPropRec"

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

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

Test "tutorial/075_sortElimProp2Rec"

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

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

Test "tutorial/076_boolRecEqns"

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

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

Test "tutorial/077_prodRecEqns"

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

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

Test "tutorial/078_nRecReduction"

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

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

Test "tutorial/079_listRecReduction"

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

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

Test "tutorial/080_RBTree.id_spec"

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

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

Test "tutorial/081_And.right"

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

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

Test "tutorial/082_Prod.snd"

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

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

Test "tutorial/083_PProd.snd"

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

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

Test "tutorial/084_PSigma.snd"

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

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

Test "tutorial/085_projOutOfRange"

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

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

stderr:

REJECT: [projOutOfRange] projection index out of range

Test "tutorial/086_projNotStruct"

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

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

stderr:

REJECT: [projNotStruct] projection: not a single-constructor inductive

Test "tutorial/087_projProp1"

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

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

Test "tutorial/088_projProp2"

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

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

stderr:

REJECT: [projProp2] cannot project a Type field from a Prop structure

Test "tutorial/089_projProp3"

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

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

Test "tutorial/090_projProp4"

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

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

stderr:

REJECT: [projProp4] cannot project a Type field from a Prop structure

Test "tutorial/091_projProp5"

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

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

stderr:

REJECT: [projProp5] cannot project a Type field from a Prop structure

Test "tutorial/092_projProp6"

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

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

Test "tutorial/093_MaybeProp.mk"

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

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

Test "tutorial/094_projMaybeProp"

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

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

Test "tutorial/095_projMaybePropPast"

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

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

Test "tutorial/096_projDataIndexRec"

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

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

Test "tutorial/097_projIndexData"

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

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

stderr:

REJECT: [projIndexData] projection struct name mismatch

Test "tutorial/098_projIndexData2"

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

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

stderr:

REJECT: [projIndexData2] projection struct name mismatch

Test "tutorial/099_projRed"

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

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

Test "tutorial/100_ruleK"

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

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

Test "tutorial/101_ruleKbad"

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

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

stderr:

REJECT: [ruleKbad] theorem 21: value type does not match declared type

Test "tutorial/102_ruleKAcc"

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

Test result: ✋ rejected · exit code 1 · wall time: 9 ms · instructions: 6.0 M · max rss memory: 8.8 MB

stderr:

REJECT: [ruleKAcc] theorem 30: value type does not match declared type

Test "tutorial/103_aNatLit"

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

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

Test "tutorial/104_natLitEq"

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

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

Test "tutorial/105_proofIrrelevance"

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

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

Test "tutorial/106_proofIrrelevanceBad"

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

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

stderr:

REJECT: [proofIrrelevanceBad] def 16: value type does not match declared type

Test "tutorial/107_proofIrrelevanceWhnf"

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

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

Test "tutorial/108_unitEta1"

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

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

Test "tutorial/109_unitEta2"

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

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

Test "tutorial/110_unitEta3"

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

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

Test "tutorial/111_indexedUnitEta"

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

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

stderr:

REJECT: [indexedUnitEta] def 25: value type does not match declared type

Test "tutorial/112_structEta"

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

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

Test "tutorial/113_indexedStructEta"

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

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

stderr:

REJECT: [indexedStructEta] def 29: value type does not match declared type

Test "tutorial/114_funEta"

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

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

Test "tutorial/115_funEtaDep"

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

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

Test "tutorial/116_funEtaBad"

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

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

stderr:

REJECT: [funEtaBad] theorem 15: value type does not match declared type

Test "tutorial/117_etaRuleK"

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

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

stderr:

REJECT: [etaRuleK] def 21: value type does not match declared type

Test "tutorial/118_etaCtor"

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

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

stderr:

REJECT: [etaCtor] def 33: value type does not match declared type

Test "tutorial/119_reflOccLeft"

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

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

stderr:

REJECT: recursor `reflOccLeft.rec` has numMotives=0 but group size is 1

Test "tutorial/120_reflOccInIndex"

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

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

stderr:

REJECT: recursor `reflOccInIndex.rec` has numMotives=0 but group size is 1

Test "tutorial/121_reduceCtorParamRefl.mk"

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

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

Test "tutorial/122_reduceCtorParamRefl2.mk"

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

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

Test "tutorial/123_rTreeRec"

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

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

Test "tutorial/124_rtreeRecReduction"

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

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

Test "tutorial/125_accRecType"

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

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

Test "tutorial/126_accRecReduction"

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

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

Test "tutorial/127_accRecNoEta"

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

Test result: ✋ rejected · exit code 1 · wall time: 9 ms · instructions: 6.0 M · max rss memory: 8.9 MB

stderr:

REJECT: [accRecNoEta] theorem 30: value type does not match declared type

Test "tutorial/128_quotMkType"

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

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

Test "tutorial/129_quotIndType"

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

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

Test "tutorial/130_quotLiftType"

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

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

Test "tutorial/131_quotSoundType"

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

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

Test "tutorial/132_quotLiftReduction"

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

Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 5.2 M · max rss memory: 8.8 MB

Test "tutorial/133_quotIndReduction"

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

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

Test "tutorial/134_dup_defs"

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

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

stderr:

REJECT: duplicate declaration of dup_defs

Test "tutorial/135_dup_ind_def"

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

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

stderr:

REJECT: duplicate declaration of dup_ind_def

Test "tutorial/136_dup_ctor_def"

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

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

stderr:

REJECT: duplicate declaration of dup_ctor_def.mk

Test "tutorial/137_dup_rec_def"

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

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

stderr:

REJECT: duplicate declaration of dup_rec_def.rec

Test "tutorial/138_misnamed_rec_user"

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

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

stderr:

REJECT: recursor `misnamed_rec.not_rec` is not named `I.rec` for an inductive in this group

Test "tutorial/139_dup_rec_def2"

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

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

stderr:

REJECT: recursor `dup_rec_def2.not_rec` is not named `I.rec` for an inductive in this group

Test "tutorial/140_dup_ctor_rec"

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

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

stderr:

REJECT: duplicate declaration of dup_ctor_rec.rec

Test "tutorial/141_DupConCon"

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

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

stderr:

REJECT: duplicate declaration of dup_ind_con_con.mk

Test "undecidability/alg-conv-trans-acc"

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

Test result: ✋ rejected · exit code 1 · wall time: 8 ms · instructions: 16.8 M · max rss memory: 10.8 MB

stderr:

REJECT: [trans] theorem 199: value type does not match declared type

Test "undecidability/alg-conv-trans-acc-left"

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

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

Test "undecidability/alg-conv-trans-acc-right"

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

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

Test "undecidability/alg-conv-trans-quot"

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

Test result: ✋ rejected · exit code 1 · wall time: 9 ms · instructions: 5.3 M · max rss memory: 8.9 MB

stderr:

REJECT: [trans] theorem 26: value type does not match declared type

Test "undecidability/alg-conv-trans-quot-left"

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

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

Test "undecidability/alg-conv-trans-quot-left-def"

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

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

Test "undecidability/alg-conv-trans-quot-right"

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

Test result: 👍 accepted · exit code 0 · wall time: 8 ms · instructions: 5.4 M · max rss memory: 8.8 MB

Test "undecidability/subject-reduction-redex"

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

Test result: 👍 accepted · exit code 0 · wall time: 9 ms · instructions: 17.7 M · max rss memory: 10.9 MB

Test "undecidability/subject-reduction-reduct"

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

Test result: ✋ rejected · exit code 1 · wall time: 9 ms · instructions: 16.9 M · max rss memory: 10.9 MB

stderr:

REJECT: [reduct] application argument type mismatch