An independent Lean 4 kernel in Haskell, and a checker for Lean exports. Re-derives every recursor, validates the Nat primitives, and agrees with Tenet on every rejection. No dependencies beyond GHC. Apache-2.0.
Haskell Updated 19 days ago 1 commits
nova-coder|Mirror: keithadler/tenet-hs (⭐0)
19 days agoAbout
An independent Lean 4 kernel in Haskell, and a checker for Lean exports. Re-derives every recursor, validates the Nat primitives, and agrees with Tenet on every rejection. No dependencies beyond GHC. Apache-2.0.
Readme