{-# OPTIONS --cubical-compatible --safe #-}
module Reflection.TCM where
import Agda.Builtin.Reflection as Builtin
open import Reflection.AST.Term
import Reflection.TCM.Format as Format
open Builtin public
using (ErrorPart; strErr; termErr; nameErr)
open Builtin public
using
( TC; bindTC; unify; typeError; inferType; checkType
; normalise; reduce
; catchTC; quoteTC; unquoteTC
; getContext; extendContext; inContext; freshName
; declareDef; declarePostulate; defineFun; getType; getDefinition
; blockOnMeta; commitTC; isMacro; withNormalisation
; debugPrint; noConstraints; runSpeculative
; Blocker; blockerMeta; blockerAny; blockerAll; blockTC
)
renaming (returnTC to pure)
open Format public
using (typeErrorFmt; debugPrintFmt; errorPartFmt)
newMeta : Type → TC Term
newMeta = checkType unknown