Directories
¶
| Path | Synopsis |
|---|---|
|
Example cubical demonstrates cubical type theory features.
|
Example cubical demonstrates cubical type theory features. |
|
Example inductive demonstrates inductive types and their eliminators.
|
Example inductive demonstrates inductive types and their eliminators. |
|
Example typecheck demonstrates basic type checking with the HoTT kernel.
|
Example typecheck demonstrates basic type checking with the HoTT kernel. |
Click to show internal directories.
Click to hide internal directories.