Module logos_env 

A LOGOS context replayed into the core: every declaration, in dependency order, admitted by Theory::Logos’s checks, with the core’s verdict for each.

A Context keeps its declarations in maps with no order, so the order is the dependency order of the globals each declaration names: the strongly connected components of that graph, dependencies first. A component of several inductive types is one mutual block; any other cycle is reported, never broken.

Inductive types are admitted LOGOS’s way, without generated recursors (match eliminates), and with Lean’s checks on each constructor: the arity is a type ending in a sort; a constructor’s type is a type whose parameter binders are the family’s, whose fields live in sorts at most the family’s unless the family is a proposition, and whose result is the family applied to exactly its parameters and then indices that do not mention the block; it takes the family’s universe parameters in the family’s order; and strict positivity holds (the Term kernel’s own check, positivity::check_positivity_mutual_resolved). The block’s recursive and reflexive shape and its irrelevant universe parameters are recorded. Definitions, theorems and axioms go through the core’s ordinary declaration checks; the certified quotient is installed whole.

Structs

Replayed

One declaration’s verdict in the replay.

Enums

Declaration

A declaration as the core admits it, in the Term forms a Context registers. params are its universe parameters, in the order its constants take levels.

Functions

admit

Admits one declaration, or one mutual block of inductive families, into a kernel built by Kernel::logos over ctx: the core’s verdict on it.

candidate_axiom

The axiom a door of ctx puts to the core, its type stored and its levels read as candidate_definition reads them.

candidate_block

The block of inductive families a door of ctx puts to the core. Each arity is stored as ctx stores it, and each member takes the stated telescope or its stored arity’s level variables. A constructor’s bare reference to a member stands at that member’s telescope, and one to anything else at the level ctx gives it.

candidate_definition

The definition a door of ctx puts to the core: its terms as ctx stores them (Context::stored_term) and the telescope the door gives it, the stated one or the level variables of the stored type and then of the body (term’s rules 1 and 4).

replay

Replays every declaration of ctx into a Kernel::logos kernel.