Elaborator (cooltt.Frontend.Elaborator)

module CS := ConcreteSyntax

module S := Core.Syntax

module RM := Core.Monads.RefineM

module D := Core.Domain

val chk_tp : CS.con -> Core.Tactic.Tp.tac

val chk_tp_in_tele : CS.cell list -> CS.con -> Core.Tactic.Tp.tac

val chk_tm : CS.con -> Core.Tactic.Chk.tac

val chk_tm_in_tele : CS.cell list -> CS.con -> Core.Tactic.Chk.tac

val syn_tm : ?elim_total:bool -> CS.con -> Core.Tactic.Syn.tac

val modifier : CS.con -> Core.Namespace.pattern RM.m