Lean 4 Models and Proofs for the Semantic Keywords in X.
Install Elan and add its bin directory to
PATH. Lake uses the compiler pinned in lean-toolchain.
lake build| Keyword | Module | Contract |
|---|---|---|
pure |
Pure | Observable-state preservation |
unique |
Unique | Exclusive borrowing |
invariant |
Invariant | Checked construction and mutation |
static |
Static | Evaluation-preserving specialization |
memoise |
Memoise | Cache validity and result preservation |
become |
Become | Constant-depth tail transfer |
multi |
Multi | Unique typed overload selection |
throws |
Throws | Error propagation and handling |
parallel |
Parallel | Range coverage and state preservation |
layout |
Layout | Logical AoS/SoA equivalence |