Lean aims to bring two worlds together
"By relieving the brain of all unnecessary work, a good notation sets it free to concentrate on more advanced problems, and in effect increases the mental power of the race." – A. N. Whitehead
Lean has an efficient bytecode interpreter
by tacinstructs Lean to use
tac : tactic unitto synthesize the missing term.
They want to avoid quotations, and gloss over the distinction between object and meta expressions.
back.lean: simple Lean tactic for list membership goals using backward chaining.
back_trace.lean: adds tracing to the previous tactic.
back_inplace.lean: same example implemeted on top of the
builtin.lean: same example using the builtin backward chaining tactic.
ematch.lean: same example using heuristic instantiation. Actually, this one is not a form of backward chaining.
builtin_ac.lean: Lean has builtin support for associative commutative operators, but this is not the point of this exercise.
flat_assoc.lean: a tactic to "flatten" nested applications of associative operators. This tactic uses only basic primitives.
flat_assoc_trace.lean: tracing tactic execution.
ac_by_simp.lean: simplifier demo.
smt_goalcontains the state of the SMT "gadgets" for a particular goal.
"Attaching more state to
tactic ==> smt_tactic
tacticthat does not change the set of hypotheses can be easily lifted because they do not invalidate the
induction) can be lifted, but the affected
smt_goal's are reconstructed from scratch.
lean --compile hello.lean ./hello "Hello Lean!"
able to use:
No need to configure; convention over configuration
lean --compile my_source_code.lean
environment.fold), type inference (
tactic.infer_type), unification (
tactic.doc_stringretrieves the doc string for a given declaration.