Directories
¶
| Path | Synopsis |
|---|---|
|
Package ast defines the abstract syntax tree for the HoTT kernel.
|
Package ast defines the abstract syntax tree for the HoTT kernel. |
|
Package core implements definitional equality checking (conversion) for the HoTT kernel.
|
Package core implements definitional equality checking (conversion) for the HoTT kernel. |
|
Package elab provides elaboration from surface syntax to core terms.
|
Package elab provides elaboration from surface syntax to core terms. |
|
Package eval implements Normalization by Evaluation (NbE) for the HoTT kernel.
|
Package eval implements Normalization by Evaluation (NbE) for the HoTT kernel. |
|
Package parser provides S-expression parsing for the HoTT kernel.
|
Package parser provides S-expression parsing for the HoTT kernel. |
|
Package unify implements unification for type inference and elaboration.
|
Package unify implements unification for type inference and elaboration. |
Click to show internal directories.
Click to hide internal directories.