λ littlelean

what's in the box: def (recursion, | pattern => … alternatives), inductive, namespace/open, match, fun/(· + 1), if/let, Nat/Int/Bool/String/Char/List/Option/tuples, ∀ x ∈ xs, ∀ n < k, #eval, #check, theorem/example.
what isn't: dependent types, a kernel, real tactics, structure, do. Any tactic block is read as "evaluate the statement" — sorry is flagged, not checked. Subtraction truncates at 0 unless the file mentions Int. For the real thing, paste into live.lean-lang.org.