mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
1361d733a6
This PR makes the external checker lean4checker available as the existing `leanchecker` binary already known to elan, allowing for out-of-the-box access to it. --------- Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
13 lines
453 B
Plaintext
13 lines
453 B
Plaintext
leanchecker found a problem in LeanCheckerTests.ReplaceAxiom
|
|
uncaught exception: (kernel) application type mismatch
|
|
False.elim @propext
|
|
argument has type
|
|
∀ {a b : Prop}, Iff a b → Eq a b
|
|
but function has type
|
|
False →
|
|
∀ (x y z n : Nat),
|
|
instLTNat.lt 0 x →
|
|
instLTNat.lt 0 y →
|
|
instLTNat.lt 0 z →
|
|
instLTNat.lt 2 n → Ne (instHAdd.hAdd (instHPow.hPow x n) (instHPow.hPow y n)) (instHPow.hPow z n)
|