Module logos_tc 

LOGOS’s Calculus of Inductive Constructions in the core: the rules Theory::Logos adds to the substitution checker.

The judgments are the Term kernel’s (type_checker.rs, reduction.rs), stated over the core’s hash-consed DAG:

• a literal’s type is LOGOS’s carrier (Int, Nat, Float, Text, Duration, Date, Moment);
• match d return m with cs takes the inductive family from d’s type, accepts a motive that is a family over that type and its indices (or a bare type, read as the constant family), owes a case for every constructor or for exactly those d’s indices allow, checks each case against the constructor’s fields, refuses an elimination out of SProp into a relevant sort and a large elimination of a family that is a proposition at some instance of its levels (unless it is a subsingleton), and has the motive applied to d’s indices and d as its type. It ι-reduces once d is in constructor form (a Nat literal is Zero or Succ, an Int literal Int_ofNat or Int_negSucc), and a single-case match on a proof of a K family or a value of a unit-like type reads its scrutinee as the constructor;
• fix f => body has the type read off body’s binders and the motive of its innermost match; in a checking position it is checked against the expected type instead, with f bound at that type. It unrolls only when the argument at the structural column the guard chose is in constructor form;
• conversion relates stuck matches, fixes and mutual fixes by congruence, an Int literal with its constructor form, and two instances of a cumulative inductive that differ only in irrelevant universe parameters;
• a term of type A stands where B is expected when A ≤ B (cumulative universes, covariant in a function type’s codomain).

The declaration-time checks of LOGOS’s own design (the termination guard, strict positivity) and the computation rules of LOGOS’s builtins (integer and text operations, the validated natLe/natLt, the reflection embedding) are the Term kernel’s, applied to lifted terms through LogosState::ctx, and so are the certificates of the programs computed natively on literals (an arithmetic operation, a Nat order or equality, a division program such as Lean’s well-founded Nat.div._unary): one implementation of each, so the two kernels cannot disagree about them.

Structs

LogosState

What checking LOGOS’s theory needs beyond the store and the environment.