Module functions 

Auto-generated module

🤖 Generated with SplitRS

Constants

PROP_LEVEL

Level of Prop (= 0).

Functions

collect_level_mvars

Collect all metavariable IDs used in a level.

collect_level_params

Collect all parameter names used in a level.

dedup_levels

Collect all levels appearing in a Vec<Level>, deduplicating by structural equality.

eval_ground_level

Evaluate a ground (no params, no mvars) level to a concrete u32.

flatten_max

Flatten a level to a list of (base, offset) pairs representing max arguments.

imax_fold

Create a level that is the imax of a slice of levels, left-folded.

instantiate_level

Instantiate level parameters using a substitution.

instantiate_level_mvars

Replace level metavariables using a substitution function.

is_definitely_succ

Check if l is definitely a successor (non-zero) level. Returns true for succ(anything).

is_equivalent

Check if two levels are semantically equivalent.

is_geq

Check if l1 >= l2 (level ordering).

is_ground

Check if a level expression is ground (no parameters, no mvars).

is_leq

Check if l1 <= l2 (level ordering).

is_numeral

Check if the level is a concrete numeral (succ^n(zero)).

level_add

Bump a level by n successor applications.

level_max3

Create max(max(l1, l2), l3) and normalize.

level_min

Compute the minimum of two levels: min(l1, l2).

max_of_slice

Create a level that is the max of a slice of levels.

normalize

Normalize a universe level to canonical form.

to_offset

Decompose a level into (base, offset) where level = succ^offset(base).

type0_level

Level of Type 0 (= 1).

type1_level

Level of Type 1 (= 2).

type_level

The universe level for Type n (= succ^(n+1)(0)).