Checker "kiota" on test "con-leche"
Checker: kiota · Version: 0.1.0 · 📄 Declaration · 🔗 Source
Test: con-leche · Expected: 👍 accept · Size: 525.9 MB · Lines: 10.0 M · lean4export: 3.1.0 · Lean: 4.33.0 · Timeout: 12.0 min · 📄 Declaration · 🔗 Source
Result: 🚫 declined · exit code 2 · wall time: 3.93 s · instructions: 49.0 G · max rss memory: 362.1 MB · run 2026-10-24 16:26:28 UTC
stderr:
[decl #100] def Bool.ctorIdx
[decl #200] theorem Nat.mod_lt
[decl #300] def Acc.recOn
[decl #400] def BitVec.casesOn
[decl #500] theorem _private.Init.Data.Nat.Div.Basic.0.Nat.modCore.go.fuel_congr
[decl #600] def _private.Init.Data.Nat.Basic.0.Nat.le_of_sub_le_sub_right.match_1_1
[decl #700] def List.reverseAux
[decl #800] theorem Nat.Internal.Linear.Poly.denote_insert
[decl #900] theorem Nat.div_lt_iff_lt_mul
[decl #1000] def Lean.Omega.Constraint.upperBound
[decl #1100] def _private.Init.Data.Int.Order.0.Int.lt_iff_le_and_ne.match_1_3
[decl #1200] theorem List.zipWith_nil_right
[decl #1300] theorem Nat.div_mul_le_self
[decl #1400] theorem Int.add_emod_emod
[decl #1500] def _private.Init.SimpLemmas.0.and_assoc.match_1_1
[decl #1600] def String.toByteArray
[decl #1700] theorem Bool.instDecidableForallOfDecidablePred._proof_2
[decl #1800] def Std.IsPreorder.of_le._auto_1
[decl #1900] def instTransEq_1
[decl #2000] theorem UInt8.and_le_right
[decl #2100] def Array.foldl
[decl #2200] theorem _private.Init.Data.BitVec.Lemmas.0.BitVec.getLsbD_shiftLeft._simp_1_1
[decl #2300] def _private.Init.Data.Nat.Lemmas.0.Nat.sub_min_sub_right.match_1_1
[decl #2400] theorem List.push_append_toArray
[decl #2500] theorem _private.Init.Data.String.Decode.0.String.toBitVec_getElem_utf8EncodeChar_zero_of_utf8Size_eq_one._simp_1_2
[decl #2600] theorem _private.Init.Data.ByteArray.Bootstrap.0.List.toList_data_toByteArray.toList_push
[decl #2700] theorem _private.Init.Data.BitVec.Lemmas.0.BitVec.toNat_twoPow._proof_1_2
[decl #2800] theorem BitVec.cons_append._proof_2
[decl #2900] theorem _private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.parseFirstByte_utf8EncodeChar_eq_threeMore
[decl #3000] theorem ByteArray.extract_eq_empty_iff._simp_1
[decl #3100] theorem Classical.not_forall
[decl #3200] def System.Platform.numBits
[decl #3300] def _private.Init.Data.Nat.Power2.Basic.0.Nat.isPowerOfTwo_mul_two_of_isPowerOfTwo.match_1_1
[decl #3400] def Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew?
[decl #3500] def ConLeche.Level.succ.noConfusion
[decl #3600] theorem _private.ConLeche.Kernel.PropWhen.0.ConLeche.PropWhenRepr.two.injEq
[decl #3700] def _private.ConLeche.Kernel.PropWhen.0.ConLeche.instHashablePropWhenRepr.hash.match_1
[decl #3800] def Std.DHashMap.contains
[decl #3900] def ConLeche.FEnv.visibleBelow
DECLINE: [ConLeche.Expr.wscopedBP.eq_1] WHNF core depth limit: (λ Nat. (λ BitVec #0. Fin.val (HPow.hPow .{0,0,0} Nat Nat Nat (instHPow .{0,0} Nat Nat (instPowNat .{0} Nat instNatPowNat)) (OfNat.ofNat .{0} Nat 2 (instOfNatNat 2)) #1) (BitVec.toFin #1 #0))) (OfNat.ofNat .{0} Nat 64 (instOfNatNat 64)) (UInt64.toBitVec (ConLeche.hash32 (mixHash (OfNat.ofNat .{0} UInt64 3 (UInt64.instOfNat 3)) (Hashable.hash .{succ(0)} Nat instHashableNat #0))))