Core.Monads
All the monads in this file keep track of a cofibration theory.
module D := CodeUnit.Domain
module S := CodeUnit.Syntax
module St := RefineState
module CmpM : sig ... end
The "computation" monad; contains enough state to run computations in the semantic domain, does not contain a variable environment or anything that would be needed for evaluation.
module EvM : sig ... end
The "evaluation" monad; like the computation monad but keeps a variable environment.
module ConvM : sig ... end
The conversion environment keeps track of De Bruijn indices for use in conversion checking.
module QuM : sig ... end
The quotation environment keeps track of De Bruijn indices for quotation.
module RefineM : sig ... end
The elaboration monad is the "maximal" monad that can run code from any of the other monads.