Module logos 

LOGOS’s own terms in the core’s store: lower takes a Term of LOGOS’s Calculus of Inductive Constructions to an ExprId, and lift takes it back.

Named variables become de Bruijn indices, a global becomes a constant (one name component, as written), and LOGOS’s universes become levels: Prop is 0, Type n is n + 1, SProp is super::level::LevelNode::SProp. match, fix and mutual fix are their own nodes, and the literals keep their LOGOS meaning (Nat and Text as the core’s Nat and string literals, the rest as Lit). An annotation is transparent and is not kept; a hole is not a kernel term and is refused.

lift names a variable after the depth of its binder (v0 outermost), so a lifted term is α-equivalent to the term that was lowered, and lowering it again gives the same id. It names the kernel’s local i fvar{i}, which lower_open takes back to that local.

Enums

LowerError

Why a term has no image in the core.

Functions

explicit_levels

The levels the Term kernel’s application rule infers for a bare reference to a universe-polymorphic declaration (type_checker::implicit_levels_for_head), written out. The declaration’s level parameters become metavariables; left to right, each argument whose domain mentions one solves it from the argument’s type; a head whose every level is solved becomes Const at those levels. A head left with an unsolved level stays a bare reference, which the core refuses rather than guesses at.

level_telescope

A global’s universe parameters and type: its explicit level telescope, or else the level variables its type mentions, which the Term kernel reads as bound by the declaration.

lift

The LOGOS term for a closed core expression.

lift_level

The LOGOS universe for a core level.

lower

The core expression for a closed LOGOS term.

lower_open

The core expression for a LOGOS term over the kernel’s locals, named as lift names them.

lower_universe

The core level for a LOGOS universe.