Core (cooltt.Core)

module CodeUnit : sig ... end

module CofBuilder : sig ... end

module CofThy : sig ... end

module CofVar : sig ... end

module Conversion : sig ... end

The purpose of this module is to check whether two well-typed objects are equal or not. The semantics are that all definitions are unfolded.

module Debug : sig ... end

module Dim : sig ... end

module DimProbe : sig ... end

module Domain : sig ... end

module DomainData : sig ... end

module Ident : sig ... end

module Log : sig ... end

module Monads : sig ... end

module Namespace : sig ... end

module Quote : sig ... end

module RefineEnv : sig ... end

module RefineError : sig ... end

module RefineErrorData : sig ... end

module RefineMonad : sig ... end

module RefineState : sig ... end

module Refiner : sig ... end

This is the basis of trusted inference rules for cooltt. This module also contains some auxiliary tactics, but these don't need to be trusted so they should be moved elsewhere.

module Scope : sig ... end

module Scopes : sig ... end

module Semantics : sig ... end

module Splice : sig ... end

module Syntax : sig ... end

module SyntaxData : sig ... end

module SyntaxPrecedence : sig ... end

module Tactic : sig ... end

module TermBuilder : sig ... end

A language for building terms without doing De Bruijn arithmetic. This module contains constructors * not only for the primitives of cubical type theory, but also for the more complex derived forms -- * for instance, the algorithm of coercion and composition in various type connectives.