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