brief intro to lean4 core

Stream: lean4

[Ping J]

disclaimer: I am by no means an lean4 expert, and this brief is not for experts, just a doc I wished to see 2 weeks ago. I spent some time reading code in lean4 core and want to write sth for google to index.

a dive into lean4 core (lean-prover/lean4)

the core 2 things: type-dependent arrow (->) and inductive type

set up a working environment and make a full build of the codebase. so hints and links can be conveniently accessed. lake exe cache get can usually save compile time.

everything ending with M is a monad, or state, to keep track of stuff and allow ordinary programming in a purely functional language.

the 1st file in the hierarchy is init/prelude.lean

if you find code hard to read, Sebastian Ulrich's papers is worth a read.

Universe level (Sort _) is used for nearly technical purposes. can skip unless main usecase is category theory.

structure of codebase

start reading src/Elab. it elaborates the syntax into an Expr. a glimpse at Expr.lean can clear things.

src/Compiler is purely for functional programming. everything up to theory verification is done in Elab. if you are mainly interested in this part, ir_interpreter.cpp is a standalone interpreter.

a keyword first goes through parsing (syntax, which is almost reg expression), then assigned a function to elab it.

[Henrik Böving]

Google doesn't index the Lean Zulip to the best of our knowledge

[Henrik Böving]

And what you are writing is also partially wrong for example lake exe cache get doesn't work in core and syntax covers a much more powerful class of languages than regular expressions.