Expand description
The checked portable core: every expression carries its type and every operator its source semantics. Emitters consume it; the renaming passes give each target unique, legal local names.
The JSON form is the JavaScript runtime’s checked program, except that
declarations is an array and items refer to declarations by name.
Structs§
- Binder
- Case
- Comparison
- Ctor
- Data
Decl - Expr
- Field
- FnDecl
- Hints
- Main
- Param
- Plan
Case - Program
- A checked portable-core program.
- Proof
- Scope
- A per-declaration name supply: target-legal, unique, deterministic.
- Split
- Theorem
Decl
Enums§
- ByZero
- What division by zero does: abort (JavaScript, Rust) or yield a total value (Lean, Rocq).
- Decl
- Effect
- Item
- A program item: a declaration, named by its full name, or a module.
- LitValue
- A literal’s value: numerals and strings are text, booleans are booleans.
- Node
- Pattern
- A single-level match pattern.
- Plan
- Prop
- Semantics
- Arithmetic semantics: exact on unbounded integers, checked (aborting) machine arithmetic, truncated natural subtraction, or IEEE-754 binary64 arithmetic on JavaScript Numbers.
Functions§
- contains_
kind - True when any expression of the given kind occurs in the tree.
- prop_
contains_ kind - True when any expression of the given kind occurs in the proposition.
- prop_
exprs - The expressions of a proposition, left to right.
- rename_
expr - Renames every binder in an expression;
envmaps source names to target names. - rename_
function - A function’s parameters and body with target local names.
- rename_
main - The main effects with target local names.
- rename_
prop - rename_
theorem - A theorem’s binders, proposition and proof plan with target local names.
- tail_
loop - Whether a function lifted from a loop calls itself only in tail position.