# per v5.3.21 - Table of Contents

The Per Programming Language

## Modules

- [Per.AST](Per.AST.md): Abstract Syntax Tree structures for the Per compiler.

- [Per.AST.And](Per.AST.And.md): Logical AND formula.
- [Per.AST.App](Per.AST.App.md): Function application.
- [Per.AST.AppFormula](Per.AST.AppFormula.md): Formula application (at-sign).
- [Per.AST.Bool](Per.AST.Bool.md): Boolean type.
- [Per.AST.DeclForeign](Per.AST.DeclForeign.md): A foreign function declaration.
- [Per.AST.DeclTypeSignature](Per.AST.DeclTypeSignature.md): A type signature declaration (axiom).
- [Per.AST.DeclValue](Per.AST.DeclValue.md): A value declaration with name, type, expression, and optional guards/WHERE clauses.
- [Per.AST.Dir](Per.AST.Dir.md): Direction (0 or 1).
- [Per.AST.Empty](Per.AST.Empty.md): Empty type.
- [Per.AST.FalseConstant](Per.AST.FalseConstant.md): False constant (0₂).
- [Per.AST.Field](Per.AST.Field.md): Field projection of a record.
- [Per.AST.Fst](Per.AST.Fst.md): First projection of a pair.
- [Per.AST.Glue](Per.AST.Glue.md): Glue type.
- [Per.AST.GlueElem](Per.AST.GlueElem.md): GlueElem term.
- [Per.AST.HComp](Per.AST.HComp.md): Homogeneous composition operation.
- [Per.AST.Hole](Per.AST.Hole.md): A placeholder hole.
- [Per.AST.Id](Per.AST.Id.md): Identity type.
- [Per.AST.IdJ](Per.AST.IdJ.md): Identity J-eliminator.
- [Per.AST.Inc](Per.AST.Inc.md): inc operation.
- [Per.AST.IndBool](Per.AST.IndBool.md): IndBool eliminator.
- [Per.AST.IndEmpty](Per.AST.IndEmpty.md): IndEmpty eliminator.
- [Per.AST.IndUnit](Per.AST.IndUnit.md): IndUnit eliminator.
- [Per.AST.IndW](Per.AST.IndW.md): IndW eliminator.
- [Per.AST.Interval](Per.AST.Interval.md): Interval type I.
- [Per.AST.Lam](Per.AST.Lam.md): A lambda abstraction.
- [Per.AST.Let](Per.AST.Let.md): A let-expression.
- [Per.AST.Module](Per.AST.Module.md): A module containing a name and declarations.
- [Per.AST.Neg](Per.AST.Neg.md): Logical NEG formula.
- [Per.AST.Neutral](Per.AST.Neutral.md): Neutral term with its type.
- [Per.AST.Or](Per.AST.Or.md): Logical OR formula.
- [Per.AST.Ouc](Per.AST.Ouc.md): ouc operation.
- [Per.AST.PLam](Per.AST.PLam.md): Path lambda abstraction.
- [Per.AST.Pair](Per.AST.Pair.md): A pair of terms.
- [Per.AST.Partial](Per.AST.Partial.md): Partial type.
- [Per.AST.PartialP](Per.AST.PartialP.md): PartialP type.
- [Per.AST.PathP](Per.AST.PathP.md): Path type.
- [Per.AST.Pi](Per.AST.Pi.md): A dependent function type.
- [Per.AST.Refl](Per.AST.Refl.md): Reflexivity term.
- [Per.AST.Sigma](Per.AST.Sigma.md): A dependent pair type.
- [Per.AST.Snd](Per.AST.Snd.md): Second projection of a pair.
- [Per.AST.Star](Per.AST.Star.md): Star term (unit constant).
- [Per.AST.Sub](Per.AST.Sub.md): Sub type.
- [Per.AST.Sup](Per.AST.Sup.md): sup term (W-type constructor).
- [Per.AST.System](Per.AST.System.md): System term (map of face -> expr).
- [Per.AST.Transp](Per.AST.Transp.md): Transport operation.
- [Per.AST.TrueConstant](Per.AST.TrueConstant.md): True constant (1₂).
- [Per.AST.Type](Per.AST.Type.md): A type at a given cosmos and level.
- [Per.AST.Unglue](Per.AST.Unglue.md): Unglue term.
- [Per.AST.Unit](Per.AST.Unit.md): Unit type.
- [Per.AST.Universe](Per.AST.Universe.md): A universe type at a given level.
- [Per.AST.Var](Per.AST.Var.md): A variable.
- [Per.AST.W](Per.AST.W.md): W-type.
- [Per.Codegen](Per.Codegen.md): Translates Per.AST into Erlang Abstract Format.

- [Per.Compiler](Per.Compiler.md): Main entry point for the Per compiler.

- [Per.DNF](Per.DNF.md): DNF (Disjunctive Normal Form) solver for cubical formulas.
Used for solving face constraints and checking equivalence of formulas.

- [Per.Desugar](Per.Desugar.md): Desugaring pass for the Per AST.
Simplifies surface language constructs into core language terms.

- [Per.Layout](Per.Layout.md): Layout resolver for the Per language.
Handles indentation-based block structure (off-side rule).

- [Per.Lexer](Per.Lexer.md): Lexer for the Per language.
Converts source text into a list of tokens.

- [Per.Lexer.Agda](Per.Lexer.Agda.md): Lexer for Agda syntax.

- [Per.Parser](Per.Parser.md): Parser for the Per language.
Converts tokens into an AST (Abstract Syntax Tree).

- [Per.Parser.Agda](Per.Parser.Agda.md)
- [Per.Typechecker](Per.Typechecker.md): Core typechecker for the Per language, implementing cubical type theory.
Includes evaluation, conversion checking, and type checking.

- [Per.Typechecker.Env](Per.Typechecker.Env.md): Typechecking environment.
- [Prof](Prof.md): Profiling utility for the Per compiler.
Used to measure execution time of different compilation phases.

## Mix Tasks

- [mix per.base](Mix.Tasks.Per.Base.md)
- [mix per.compile](Mix.Tasks.Per.Compile.md)
- [mix per.repl](Mix.Tasks.Per.Repl.md)
- [mix per.test](Mix.Tasks.Per.Test.md)

