Module 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 Serialize : 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.