API Reference per v#5.3.21
Copy MarkdownModules
Abstract Syntax Tree structures for the Per compiler.
Logical AND formula.
Function application.
Formula application (at-sign).
Boolean type.
A foreign function declaration.
A type signature declaration (axiom).
A value declaration with name, type, expression, and optional guards/WHERE clauses.
Direction (0 or 1).
Empty type.
False constant (0₂).
Field projection of a record.
First projection of a pair.
Glue type.
GlueElem term.
Homogeneous composition operation.
A placeholder hole.
Identity type.
Identity J-eliminator.
inc operation.
IndBool eliminator.
IndEmpty eliminator.
IndUnit eliminator.
IndW eliminator.
Interval type I.
A lambda abstraction.
A let-expression.
A module containing a name and declarations.
Logical NEG formula.
Neutral term with its type.
Logical OR formula.
ouc operation.
Path lambda abstraction.
A pair of terms.
Partial type.
PartialP type.
Path type.
A dependent function type.
Reflexivity term.
A dependent pair type.
Second projection of a pair.
Star term (unit constant).
Sub type.
sup term (W-type constructor).
System term (map of face -> expr).
Transport operation.
True constant (1₂).
A type at a given cosmos and level.
Unglue term.
Unit type.
A universe type at a given level.
A variable.
W-type.
Translates Per.AST into Erlang Abstract Format.
Main entry point for the Per compiler.
DNF (Disjunctive Normal Form) solver for cubical formulas. Used for solving face constraints and checking equivalence of formulas.
Desugaring pass for the Per AST. Simplifies surface language constructs into core language terms.
Layout resolver for the Per language. Handles indentation-based block structure (off-side rule).
Lexer for the Per language. Converts source text into a list of tokens.
Lexer for Agda syntax.
Parser for the Per language. Converts tokens into an AST (Abstract Syntax Tree).
Core typechecker for the Per language, implementing cubical type theory. Includes evaluation, conversion checking, and type checking.
Typechecking environment.
Profiling utility for the Per compiler. Used to measure execution time of different compilation phases.