Expand description
Data structures for managing toplevel declarations in the type theory.
Specifically, notebooks will produce TopDecl::Type declarations.
Structs§
- Def
- A toplevel declaration of a term judgment
- DefConst
- A toplevel declaration of a term in the empty context.
- Theory
- A theory supported by doublett.
- Toplevel
- Storage for toplevel declarations.
- Type
- A toplevel declaration of a type.
Enums§
- TopDecl
- A toplevel declaration.
Functions§
- std_
theories - Construct a library of standard theories