Module Core.Quote

The purpose of this module is to transform semantic objects into syntactic objects as efficiently as possible.

module D := CodeUnit.Domain
module S := CodeUnit.Syntax
val quote_con : D.tp -> D.con -> S.t Monads.quote
val quote_tp : D.tp -> S.tp Monads.quote
val quote_tele : D.tele -> S.tele Monads.quote
val quote_kan_tele : D.kan_tele -> S.kan_tele Monads.quote
val quote_cut : D.cut -> S.t Monads.quote
val quote_cof : D.cof -> S.t Monads.quote
val quote_dim : D.dim -> S.t Monads.quote