This material is a proof-of-concept code of my hypothesis that writing a prover will be much easier if I take a proof assistant as its implementation language. An explanatory article about this project will be available soon at techbookfest 2019 spring.

I didn't implement a large part of language features which a proof assistant needs for being called a proof assistant. Instead they are realized by free riding on the metalanguage; I didn't implement:

• parser (it's a DSL)
• binding structure (use HOAS)
• type checker (Lean's type checker checks it)
• type inference (Lean's unifier infers it)
• (efficient) evaluator (use the NbE technique)
• tactic language (Lean's tactic language serves it)

That's why the code is very small (< 300 LoC).

I separate from the main file (hol.lean) some codes I additionally wrote to write my article. Mainly looking at hol.lean should suffice if you know its technical backgrounds already.