    module Agda.TypeChecking.Monad.Builtin
      ( module Agda.TypeChecking.Monad.Builtin
      , module Agda.Syntax.Builtin  -- The names are defined here.
      ) where

    import Control.Monad.Except         ( MonadError(..), ExceptT )
    import Control.Monad.IO.Class       ( MonadIO(..) )
    import Control.Monad.Reader         ( ReaderT )
    import Control.Monad.State          ( StateT )
    import Control.Monad.Trans.Identity ( IdentityT )
    import Control.Monad.Trans.Maybe
    import Control.Monad.Writer         ( WriterT )

    import Data.Function ( on )
    import qualified Data.Map as Map
    import Data.Set (Set)

    import Agda.Syntax.Common
    import Agda.Syntax.Position
    import Agda.Syntax.Literal
    import Agda.Syntax.Builtin
    import Agda.Syntax.Internal as I
    import Agda.TypeChecking.Monad.Base
    -- import Agda.TypeChecking.Functions  -- LEADS TO IMPORT CYCLE
    import Agda.TypeChecking.Substitute

    import Agda.Utils.Functor
    import Agda.Utils.Lens
    import Agda.Utils.ListT
    import Agda.Utils.Monad
    import Agda.Utils.Maybe
    import Agda.Utils.Singleton
    import Agda.Utils.Tuple
    import Agda.Utils.Update

    import Agda.Utils.Impossible

    class ( Functor m
          , Applicative m
          , Monad m
          ) => HasBuiltins m where
      getBuiltinThing :: SomeBuiltin -> m (Maybe (Builtin PrimFun))

      default getBuiltinThing :: (MonadTrans t, HasBuiltins n, t n ~ m) => SomeBuiltin -> m (Maybe (Builtin PrimFun))
      getBuiltinThing = n (Maybe (Builtin PrimFun)) -> m (Maybe (Builtin PrimFun))
    n (Maybe (Builtin PrimFun)) -> t n (Maybe (Builtin PrimFun))
    forall (m :: * -> *) a. Monad m => m a -> t m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (n (Maybe (Builtin PrimFun)) -> m (Maybe (Builtin PrimFun)))
    -> (SomeBuiltin -> n (Maybe (Builtin PrimFun)))
    -> SomeBuiltin
    -> m (Maybe (Builtin PrimFun))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SomeBuiltin -> n (Maybe (Builtin PrimFun))
    forall (m :: * -> *).
    HasBuiltins m =>
    SomeBuiltin -> m (Maybe (Builtin PrimFun))
    getBuiltinThing

    instance HasBuiltins m => HasBuiltins (ChangeT m)
    instance HasBuiltins m => HasBuiltins (ExceptT e m)
    instance HasBuiltins m => HasBuiltins (IdentityT m)
    instance HasBuiltins m => HasBuiltins (ListT m)
    instance HasBuiltins m => HasBuiltins (MaybeT m)
    instance HasBuiltins m => HasBuiltins (ReaderT e m)
    instance HasBuiltins m => HasBuiltins (StateT s m)
    instance (HasBuiltins m, Monoid w) => HasBuiltins (WriterT w m)

    deriving instance HasBuiltins m => HasBuiltins (BlockT m)

    instance MonadIO m => HasBuiltins (TCMT m) where
      getBuiltinThing :: SomeBuiltin -> TCMT m (Maybe (Builtin PrimFun))
    getBuiltinThing SomeBuiltin
    b =
        (Maybe (Builtin PrimFun)
     -> Maybe (Builtin PrimFun) -> Maybe (Builtin PrimFun))
    -> TCMT m (Maybe (Builtin PrimFun))
    -> TCMT m (Maybe (Builtin PrimFun))
    -> TCMT m (Maybe (Builtin PrimFun))
    forall (m :: * -> *) a1 a2 r.
    Monad m =>
    (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
    liftM2 ((Builtin PrimFun -> Builtin PrimFun -> Builtin PrimFun)
    -> Maybe (Builtin PrimFun)
    -> Maybe (Builtin PrimFun)
    -> Maybe (Builtin PrimFun)
    forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
    unionMaybeWith Builtin PrimFun -> Builtin PrimFun -> Builtin PrimFun
    forall a. Builtin a -> Builtin a -> Builtin a
    unionBuiltin)
          (SomeBuiltin
    -> Map SomeBuiltin (Builtin PrimFun) -> Maybe (Builtin PrimFun)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup SomeBuiltin
    b (Map SomeBuiltin (Builtin PrimFun) -> Maybe (Builtin PrimFun))
    -> TCMT m (Map SomeBuiltin (Builtin PrimFun))
    -> TCMT m (Maybe (Builtin PrimFun))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
    -> TCMT m (Map SomeBuiltin (Builtin PrimFun))
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (Map SomeBuiltin (Builtin PrimFun)
     -> f (Map SomeBuiltin (Builtin PrimFun)))
    -> TCState -> f TCState
    Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
    stLocalBuiltins)
          (SomeBuiltin
    -> Map SomeBuiltin (Builtin PrimFun) -> Maybe (Builtin PrimFun)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup SomeBuiltin
    b (Map SomeBuiltin (Builtin PrimFun) -> Maybe (Builtin PrimFun))
    -> TCMT m (Map SomeBuiltin (Builtin PrimFun))
    -> TCMT m (Maybe (Builtin PrimFun))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
    -> TCMT m (Map SomeBuiltin (Builtin PrimFun))
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (Map SomeBuiltin (Builtin PrimFun)
     -> f (Map SomeBuiltin (Builtin PrimFun)))
    -> TCState -> f TCState
    Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
    stImportedBuiltins)
    {-# SPECIALIZE getBuiltinThing :: SomeBuiltin -> TCM (Maybe (Builtin PrimFun)) #-}

    -- | The trivial implementation of 'HasBuiltins', using a constant 'TCState'.
    --
    -- This may be used instead of 'TCMT'/'ReduceM' where builtins must be accessed
    -- in a pure context.
    newtype BuiltinAccess a = BuiltinAccess { forall a. BuiltinAccess a -> TCState -> a
    unBuiltinAccess :: TCState -> a }
      deriving ((forall a b. (a -> b) -> BuiltinAccess a -> BuiltinAccess b)
    -> (forall a b. a -> BuiltinAccess b -> BuiltinAccess a)
    -> Functor BuiltinAccess
    forall a b. a -> BuiltinAccess b -> BuiltinAccess a
    forall a b. (a -> b) -> BuiltinAccess a -> BuiltinAccess b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> BuiltinAccess a -> BuiltinAccess b
    fmap :: forall a b. (a -> b) -> BuiltinAccess a -> BuiltinAccess b
    $c<$ :: forall a b. a -> BuiltinAccess b -> BuiltinAccess a
    <$ :: forall a b. a -> BuiltinAccess b -> BuiltinAccess a
    Functor, Functor BuiltinAccess
    Functor BuiltinAccess =>
    (forall a. a -> BuiltinAccess a)
    -> (forall a b.
        BuiltinAccess (a -> b) -> BuiltinAccess a -> BuiltinAccess b)
    -> (forall a b c.
        (a -> b -> c)
        -> BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess c)
    -> (forall a b.
        BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess b)
    -> (forall a b.
        BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess a)
    -> Applicative BuiltinAccess
    forall a. a -> BuiltinAccess a
    forall a b. BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess a
    forall a b. BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess b
    forall a b.
    BuiltinAccess (a -> b) -> BuiltinAccess a -> BuiltinAccess b
    forall a b c.
    (a -> b -> c)
    -> BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess c
    forall (f :: * -> *).
    Functor f =>
    (forall a. a -> f a)
    -> (forall a b. f (a -> b) -> f a -> f b)
    -> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
    -> (forall a b. f a -> f b -> f b)
    -> (forall a b. f a -> f b -> f a)
    -> Applicative f
    $cpure :: forall a. a -> BuiltinAccess a
    pure :: forall a. a -> BuiltinAccess a
    $c<*> :: forall a b.
    BuiltinAccess (a -> b) -> BuiltinAccess a -> BuiltinAccess b
    <*> :: forall a b.
    BuiltinAccess (a -> b) -> BuiltinAccess a -> BuiltinAccess b
    $cliftA2 :: forall a b c.
    (a -> b -> c)
    -> BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess c
    liftA2 :: forall a b c.
    (a -> b -> c)
    -> BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess c
    $c*> :: forall a b. BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess b
    *> :: forall a b. BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess b
    $c<* :: forall a b. BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess a
    <* :: forall a b. BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess a
    Applicative, Applicative BuiltinAccess
    Applicative BuiltinAccess =>
    (forall a b.
     BuiltinAccess a -> (a -> BuiltinAccess b) -> BuiltinAccess b)
    -> (forall a b.
        BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess b)
    -> (forall a. a -> BuiltinAccess a)
    -> Monad BuiltinAccess
    forall a. a -> BuiltinAccess a
    forall a b. BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess b
    forall a b.
    BuiltinAccess a -> (a -> BuiltinAccess b) -> BuiltinAccess b
    forall (m :: * -> *).
    Applicative m =>
    (forall a b. m a -> (a -> m b) -> m b)
    -> (forall a b. m a -> m b -> m b)
    -> (forall a. a -> m a)
    -> Monad m
    $c>>= :: forall a b.
    BuiltinAccess a -> (a -> BuiltinAccess b) -> BuiltinAccess b
    >>= :: forall a b.
    BuiltinAccess a -> (a -> BuiltinAccess b) -> BuiltinAccess b
    $c>> :: forall a b. BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess b
    >> :: forall a b. BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess b
    $creturn :: forall a. a -> BuiltinAccess a
    return :: forall a. a -> BuiltinAccess a
    Monad)

    instance MonadFail BuiltinAccess where
      fail :: forall a. String -> BuiltinAccess a
    fail String
    msg = (TCState -> a) -> BuiltinAccess a
    forall a. (TCState -> a) -> BuiltinAccess a
    BuiltinAccess ((TCState -> a) -> BuiltinAccess a)
    -> (TCState -> a) -> BuiltinAccess a
    forall a b. (a -> b) -> a -> b
    $ \TCState
    _ -> String -> a
    forall a. HasCallStack => String -> a
    error String
    msg

    instance HasBuiltins BuiltinAccess where
      getBuiltinThing :: SomeBuiltin -> BuiltinAccess (Maybe (Builtin PrimFun))
    getBuiltinThing SomeBuiltin
    b = (TCState -> Maybe (Builtin PrimFun))
    -> BuiltinAccess (Maybe (Builtin PrimFun))
    forall a. (TCState -> a) -> BuiltinAccess a
    BuiltinAccess ((TCState -> Maybe (Builtin PrimFun))
     -> BuiltinAccess (Maybe (Builtin PrimFun)))
    -> (TCState -> Maybe (Builtin PrimFun))
    -> BuiltinAccess (Maybe (Builtin PrimFun))
    forall a b. (a -> b) -> a -> b
    $ \TCState
    state ->
        (Builtin PrimFun -> Builtin PrimFun -> Builtin PrimFun)
    -> Maybe (Builtin PrimFun)
    -> Maybe (Builtin PrimFun)
    -> Maybe (Builtin PrimFun)
    forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
    unionMaybeWith Builtin PrimFun -> Builtin PrimFun -> Builtin PrimFun
    forall a. Builtin a -> Builtin a -> Builtin a
    unionBuiltin
          (SomeBuiltin
    -> Map SomeBuiltin (Builtin PrimFun) -> Maybe (Builtin PrimFun)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup SomeBuiltin
    b (Map SomeBuiltin (Builtin PrimFun) -> Maybe (Builtin PrimFun))
    -> Map SomeBuiltin (Builtin PrimFun) -> Maybe (Builtin PrimFun)
    forall a b. (a -> b) -> a -> b
    $ TCState
    state TCState
    -> Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
    -> Map SomeBuiltin (Builtin PrimFun)
    forall o i. o -> Lens' o i -> i
    ^. (Map SomeBuiltin (Builtin PrimFun)
     -> f (Map SomeBuiltin (Builtin PrimFun)))
    -> TCState -> f TCState
    Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
    stLocalBuiltins)
          (SomeBuiltin
    -> Map SomeBuiltin (Builtin PrimFun) -> Maybe (Builtin PrimFun)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup SomeBuiltin
    b (Map SomeBuiltin (Builtin PrimFun) -> Maybe (Builtin PrimFun))
    -> Map SomeBuiltin (Builtin PrimFun) -> Maybe (Builtin PrimFun)
    forall a b. (a -> b) -> a -> b
    $ TCState
    state TCState
    -> Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
    -> Map SomeBuiltin (Builtin PrimFun)
    forall o i. o -> Lens' o i -> i
    ^. (Map SomeBuiltin (Builtin PrimFun)
     -> f (Map SomeBuiltin (Builtin PrimFun)))
    -> TCState -> f TCState
    Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
    stImportedBuiltins)

    -- | Run a 'BuiltinAccess' monad.
    runBuiltinAccess :: TCState -> BuiltinAccess a -> a
    runBuiltinAccess :: forall a. TCState -> BuiltinAccess a -> a
    runBuiltinAccess TCState
    s BuiltinAccess a
    m = BuiltinAccess a -> TCState -> a
    forall a. BuiltinAccess a -> TCState -> a
    unBuiltinAccess BuiltinAccess a
    m TCState
    s

    -- If Agda is changed so that the type of a literal can belong to an
    -- inductive family (with at least one index), then the implementation
    -- of split' in Agda.TypeChecking.Coverage should be changed.

    litType
      :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m)
      => Literal -> m Type
    litType :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    Literal -> m Type
    litType = \case
      LitNat Integer
    n    -> do
        _ <- m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primZero
        when (n > 0) $ void $ primSuc
        el <$> primNat
      LitWord64 Word64
    _ -> Term -> Type
    forall {a}. a -> Type'' Term a
    el (Term -> Type) -> m Term -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primWord64
      LitFloat Double
    _  -> Term -> Type
    forall {a}. a -> Type'' Term a
    el (Term -> Type) -> m Term -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primFloat
      LitChar Char
    _   -> Term -> Type
    forall {a}. a -> Type'' Term a
    el (Term -> Type) -> m Term -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primChar
      LitString Text
    _ -> Term -> Type
    forall {a}. a -> Type'' Term a
    el (Term -> Type) -> m Term -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primString
      LitQName QName
    _  -> Term -> Type
    forall {a}. a -> Type'' Term a
    el (Term -> Type) -> m Term -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primQName
      LitMeta TopLevelModuleName' Range
    _ MetaId
    _ -> Term -> Type
    forall {a}. a -> Type'' Term a
    el (Term -> Type) -> m Term -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaMeta
      where
        el :: a -> Type'' Term a
    el a
    t = Sort' Term -> a -> Type'' Term a
    forall t a. Sort' t -> a -> Type'' t a
    El (Integer -> Sort' Term
    mkType Integer
    0) a
    t

    setBuiltinThings :: BuiltinThings -> TCM ()
    setBuiltinThings :: Map SomeBuiltin (Builtin PrimFun) -> TCM ()
    setBuiltinThings Map SomeBuiltin (Builtin PrimFun)
    b = (Map SomeBuiltin (Builtin PrimFun)
     -> f (Map SomeBuiltin (Builtin PrimFun)))
    -> TCState -> f TCState
    Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
    stLocalBuiltins Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
    -> Map SomeBuiltin (Builtin PrimFun) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> a -> m ()
    `setTCLens` Map SomeBuiltin (Builtin PrimFun)
    b

    bindBuiltinName :: BuiltinId -> Term -> TCM ()
    bindBuiltinName :: BuiltinId -> Term -> TCM ()
    bindBuiltinName BuiltinId
    b Term
    x = do
      builtin <- SomeBuiltin -> TCMT IO (Maybe (Builtin PrimFun))
    forall (m :: * -> *).
    HasBuiltins m =>
    SomeBuiltin -> m (Maybe (Builtin PrimFun))
    getBuiltinThing SomeBuiltin
    b'
      case builtin of
        Just (Builtin Term
    y) -> TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ BuiltinId -> Term -> Term -> TypeError
    DuplicateBuiltinBinding BuiltinId
    b Term
    y Term
    x
        Just Prim{}      -> TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TypeError
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Just BuiltinRewriteRelations{} -> TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Maybe (Builtin PrimFun)
    Nothing          -> (Map SomeBuiltin (Builtin PrimFun)
     -> f (Map SomeBuiltin (Builtin PrimFun)))
    -> TCState -> f TCState
    Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
    stLocalBuiltins Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
    -> (Map SomeBuiltin (Builtin PrimFun)
        -> Map SomeBuiltin (Builtin PrimFun))
    -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens` SomeBuiltin
    -> Builtin PrimFun
    -> Map SomeBuiltin (Builtin PrimFun)
    -> Map SomeBuiltin (Builtin PrimFun)
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert SomeBuiltin
    b' (Term -> Builtin PrimFun
    forall pf. Term -> Builtin pf
    Builtin Term
    x)
      where b' :: SomeBuiltin
    b' = BuiltinId -> SomeBuiltin
    BuiltinName BuiltinId
    b

    bindPrimitive :: PrimitiveId -> PrimFun -> TCM ()
    bindPrimitive :: PrimitiveId -> PrimFun -> TCM ()
    bindPrimitive PrimitiveId
    b PrimFun
    pf = do
      builtin <- SomeBuiltin -> TCMT IO (Maybe (Builtin PrimFun))
    forall (m :: * -> *).
    HasBuiltins m =>
    SomeBuiltin -> m (Maybe (Builtin PrimFun))
    getBuiltinThing SomeBuiltin
    b'
      case builtin of
        Just (Builtin Term
    _) -> TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ String -> TypeError
    NoSuchPrimitiveFunction (PrimitiveId -> String
    forall a. IsBuiltin a => a -> String
    getBuiltinId PrimitiveId
    b)
        Just (Prim PrimFun
    x)    -> TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (PrimitiveId -> QName -> QName -> TypeError
    DuplicatePrimitiveBinding PrimitiveId
    b (QName -> QName -> TypeError)
    -> (PrimFun -> QName) -> PrimFun -> PrimFun -> TypeError
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` PrimFun -> QName
    primFunName) PrimFun
    x PrimFun
    pf
        Just BuiltinRewriteRelations{} -> TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Maybe (Builtin PrimFun)
    Nothing          -> (Map SomeBuiltin (Builtin PrimFun)
     -> f (Map SomeBuiltin (Builtin PrimFun)))
    -> TCState -> f TCState
    Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
    stLocalBuiltins Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
    -> (Map SomeBuiltin (Builtin PrimFun)
        -> Map SomeBuiltin (Builtin PrimFun))
    -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens` SomeBuiltin
    -> Builtin PrimFun
    -> Map SomeBuiltin (Builtin PrimFun)
    -> Map SomeBuiltin (Builtin PrimFun)
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert SomeBuiltin
    b' (PrimFun -> Builtin PrimFun
    forall pf. pf -> Builtin pf
    Prim PrimFun
    pf)
      where b' :: SomeBuiltin
    b' = PrimitiveId -> SomeBuiltin
    PrimitiveName PrimitiveId
    b

    -- | Add one (more) relation symbol to the rewrite relations.
    bindBuiltinRewriteRelation :: QName -> TCM ()
    bindBuiltinRewriteRelation :: QName -> TCM ()
    bindBuiltinRewriteRelation QName
    x =
      (Map SomeBuiltin (Builtin PrimFun)
     -> f (Map SomeBuiltin (Builtin PrimFun)))
    -> TCState -> f TCState
    Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
    stLocalBuiltins Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
    -> (Map SomeBuiltin (Builtin PrimFun)
        -> Map SomeBuiltin (Builtin PrimFun))
    -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens`
        (Builtin PrimFun -> Builtin PrimFun -> Builtin PrimFun)
    -> SomeBuiltin
    -> Builtin PrimFun
    -> Map SomeBuiltin (Builtin PrimFun)
    -> Map SomeBuiltin (Builtin PrimFun)
    forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
    Map.insertWith Builtin PrimFun -> Builtin PrimFun -> Builtin PrimFun
    forall a. Builtin a -> Builtin a -> Builtin a
    unionBuiltin (BuiltinId -> SomeBuiltin
    BuiltinName BuiltinId
    builtinRewrite) (Set QName -> Builtin PrimFun
    forall pf. Set QName -> Builtin pf
    BuiltinRewriteRelations (Set QName -> Builtin PrimFun) -> Set QName -> Builtin PrimFun
    forall a b. (a -> b) -> a -> b
    $ QName -> Set QName
    forall el coll. Singleton el coll => el -> coll
    singleton QName
    x)

    -- | Get the currently registered rewrite relation symbols.
    getBuiltinRewriteRelations :: (HasBuiltins m, MonadTCError m) => m (Set QName)
    getBuiltinRewriteRelations :: forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    m (Set QName)
    getBuiltinRewriteRelations =
      m (Set QName) -> m (Maybe (Set QName)) -> m (Set QName)
    forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
    fromMaybeM (TypeError -> m (Set QName)
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m (Set QName)) -> TypeError -> m (Set QName)
    forall a b. (a -> b) -> a -> b
    $ BuiltinId -> TypeError
    NoBindingForBuiltin BuiltinId
    builtinRewrite) m (Maybe (Set QName))
    forall (m :: * -> *). HasBuiltins m => m (Maybe (Set QName))
    getBuiltinRewriteRelations'

    -- | Get the currently registered rewrite relation symbols, if any.
    getBuiltinRewriteRelations' :: HasBuiltins m => m (Maybe (Set QName))
    getBuiltinRewriteRelations' :: forall (m :: * -> *). HasBuiltins m => m (Maybe (Set QName))
    getBuiltinRewriteRelations' = (Builtin PrimFun -> Set QName)
    -> Maybe (Builtin PrimFun) -> Maybe (Set QName)
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Builtin PrimFun -> Set QName
    forall {pf}. Builtin pf -> Set QName
    rels (Maybe (Builtin PrimFun) -> Maybe (Set QName))
    -> m (Maybe (Builtin PrimFun)) -> m (Maybe (Set QName))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SomeBuiltin -> m (Maybe (Builtin PrimFun))
    forall (m :: * -> *).
    HasBuiltins m =>
    SomeBuiltin -> m (Maybe (Builtin PrimFun))
    getBuiltinThing (BuiltinId -> SomeBuiltin
    BuiltinName BuiltinId
    builtinRewrite)
      where
      rels :: Builtin pf -> Set QName
    rels = \case
        BuiltinRewriteRelations Set QName
    xs -> Set QName
    xs
        Prim{}    -> Set QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Builtin{} -> Set QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    {-# INLINABLE getBuiltinName_ #-}
    getBuiltinName_ :: (HasBuiltins m, MonadTCError m)
      => BuiltinId -> m QName
    getBuiltinName_ :: forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m QName
    getBuiltinName_ BuiltinId
    x =
      m QName -> m (Maybe QName) -> m QName
    forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
    fromMaybeM (TypeError -> m QName
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m QName) -> TypeError -> m QName
    forall a b. (a -> b) -> a -> b
    $ BuiltinId -> TypeError
    NoBindingForBuiltin BuiltinId
    x) (m (Maybe QName) -> m QName) -> m (Maybe QName) -> m QName
    forall a b. (a -> b) -> a -> b
    $ BuiltinId -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
    getBuiltinName' BuiltinId
    x

    -- {-# INLINABLE getBuiltinName' #-}
    -- -- | Returns 'Nothing' if built-in is not bound or bound to a 'Prim' or anything other than a 'Def'.
    -- getBuiltinName' :: HasBuiltins m => BuiltinId -> m (Maybe Term)
    -- getBuiltinName' x = (getBuiltinName =<<) <$> getBuiltin' x
    --   where
    --     getBuiltinName = \case
    --       Def f [] -> Just f
    --       _        -> Nothing

    {-# INLINABLE getBuiltin #-}
    getBuiltin :: (HasBuiltins m, MonadTCError m)
               => BuiltinId -> m Term
    getBuiltin :: forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    x =
      m Term -> m (Maybe Term) -> m Term
    forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
    fromMaybeM (TypeError -> m Term
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m Term) -> TypeError -> m Term
    forall a b. (a -> b) -> a -> b
    $ BuiltinId -> TypeError
    NoBindingForBuiltin BuiltinId
    x) (m (Maybe Term) -> m Term) -> m (Maybe Term) -> m Term
    forall a b. (a -> b) -> a -> b
    $ BuiltinId -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    x

    {-# INLINABLE getBuiltin' #-}
    -- | Returns 'Nothing' if built-in is not bound or bound to a 'Prim'.
    getBuiltin' :: HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' :: forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    x = (Builtin PrimFun -> Maybe Term
    forall {pf}. Builtin pf -> Maybe Term
    getBuiltin (Builtin PrimFun -> Maybe Term)
    -> Maybe (Builtin PrimFun) -> Maybe Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<) (Maybe (Builtin PrimFun) -> Maybe Term)
    -> m (Maybe (Builtin PrimFun)) -> m (Maybe Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SomeBuiltin -> m (Maybe (Builtin PrimFun))
    forall (m :: * -> *).
    HasBuiltins m =>
    SomeBuiltin -> m (Maybe (Builtin PrimFun))
    getBuiltinThing (BuiltinId -> SomeBuiltin
    BuiltinName BuiltinId
    x)
      where
        getBuiltin :: Builtin pf -> Maybe Term
    getBuiltin = \case
          Builtin Term
    t                 -> Term -> Maybe Term
    forall a. a -> Maybe a
    Just (Term -> Maybe Term) -> Term -> Maybe Term
    forall a b. (a -> b) -> a -> b
    $ KillRangeT Term
    forall a. KillRange a => KillRangeT a
    killRange Term
    t
          Prim{}                    -> Maybe Term
    forall a. Maybe a
    Nothing
          BuiltinRewriteRelations{} -> Maybe Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    {-# INLINABLE getPrimitive' #-}
    -- | Returns 'Nothing' if primitive is not bound or bound to a 'Builtin'.
    getPrimitive' :: HasBuiltins m => PrimitiveId -> m (Maybe PrimFun)
    getPrimitive' :: forall (m :: * -> *).
    HasBuiltins m =>
    PrimitiveId -> m (Maybe PrimFun)
    getPrimitive' PrimitiveId
    x = (Builtin PrimFun -> Maybe PrimFun
    forall {a}. Builtin a -> Maybe a
    getPrim (Builtin PrimFun -> Maybe PrimFun)
    -> Maybe (Builtin PrimFun) -> Maybe PrimFun
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<) (Maybe (Builtin PrimFun) -> Maybe PrimFun)
    -> m (Maybe (Builtin PrimFun)) -> m (Maybe PrimFun)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SomeBuiltin -> m (Maybe (Builtin PrimFun))
    forall (m :: * -> *).
    HasBuiltins m =>
    SomeBuiltin -> m (Maybe (Builtin PrimFun))
    getBuiltinThing (PrimitiveId -> SomeBuiltin
    PrimitiveName PrimitiveId
    x)
      where
        getPrim :: Builtin a -> Maybe a
    getPrim = \case
          Prim a
    pf                   -> a -> Maybe a
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    pf
          Builtin{}                 -> Maybe a
    forall a. Maybe a
    Nothing
          BuiltinRewriteRelations{} -> Maybe a
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    {-# INLINABLE getPrimitive #-}
    getPrimitive :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m)
                 => PrimitiveId -> m PrimFun
    getPrimitive :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    PrimitiveId -> m PrimFun
    getPrimitive PrimitiveId
    x =
      m PrimFun -> m (Maybe PrimFun) -> m PrimFun
    forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
    fromMaybeM (TypeError -> m PrimFun
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m PrimFun)
    -> (String -> TypeError) -> String -> m PrimFun
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> TypeError
    NoSuchPrimitiveFunction (String -> m PrimFun) -> String -> m PrimFun
    forall a b. (a -> b) -> a -> b
    $ PrimitiveId -> String
    forall a. IsBuiltin a => a -> String
    getBuiltinId PrimitiveId
    x) (m (Maybe PrimFun) -> m PrimFun) -> m (Maybe PrimFun) -> m PrimFun
    forall a b. (a -> b) -> a -> b
    $ PrimitiveId -> m (Maybe PrimFun)
    forall (m :: * -> *).
    HasBuiltins m =>
    PrimitiveId -> m (Maybe PrimFun)
    getPrimitive' PrimitiveId
    x

    getPrimitiveTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m)
                     => PrimitiveId -> m Term
    getPrimitiveTerm :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    PrimitiveId -> m Term
    getPrimitiveTerm PrimitiveId
    x = (QName -> Elims -> Term
    `Def` []) (QName -> Term) -> (PrimFun -> QName) -> PrimFun -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PrimFun -> QName
    primFunName (PrimFun -> Term) -> m PrimFun -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PrimitiveId -> m PrimFun
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    PrimitiveId -> m PrimFun
    getPrimitive PrimitiveId
    x

    getPrimitiveTerm' :: HasBuiltins m => PrimitiveId -> m (Maybe Term)
    getPrimitiveTerm' :: forall (m :: * -> *).
    HasBuiltins m =>
    PrimitiveId -> m (Maybe Term)
    getPrimitiveTerm' PrimitiveId
    x = (QName -> Term) -> Maybe QName -> Maybe Term
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (QName -> Elims -> Term
    `Def` []) (Maybe QName -> Maybe Term) -> m (Maybe QName) -> m (Maybe Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PrimitiveId -> m (Maybe QName)
    forall (m :: * -> *).
    HasBuiltins m =>
    PrimitiveId -> m (Maybe QName)
    getPrimitiveName' PrimitiveId
    x

    getTerm' :: (HasBuiltins m, IsBuiltin a) => a -> m (Maybe Term)
    getTerm' :: forall (m :: * -> *) a.
    (HasBuiltins m, IsBuiltin a) =>
    a -> m (Maybe Term)
    getTerm' = SomeBuiltin -> m (Maybe Term)
    forall {m :: * -> *}.
    HasBuiltins m =>
    SomeBuiltin -> m (Maybe Term)
    go (SomeBuiltin -> m (Maybe Term))
    -> (a -> SomeBuiltin) -> a -> m (Maybe Term)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin where
      go :: SomeBuiltin -> m (Maybe Term)
    go (BuiltinName BuiltinId
    x)   = BuiltinId -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    x
      go (PrimitiveName PrimitiveId
    x) = PrimitiveId -> m (Maybe Term)
    forall (m :: * -> *).
    HasBuiltins m =>
    PrimitiveId -> m (Maybe Term)
    getPrimitiveTerm' PrimitiveId
    x

    getName' :: (HasBuiltins m, IsBuiltin a) => a -> m (Maybe QName)
    getName' :: forall (m :: * -> *) a.
    (HasBuiltins m, IsBuiltin a) =>
    a -> m (Maybe QName)
    getName' = SomeBuiltin -> m (Maybe QName)
    forall {m :: * -> *}.
    HasBuiltins m =>
    SomeBuiltin -> m (Maybe QName)
    go (SomeBuiltin -> m (Maybe QName))
    -> (a -> SomeBuiltin) -> a -> m (Maybe QName)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin where
      go :: SomeBuiltin -> m (Maybe QName)
    go (BuiltinName BuiltinId
    x)   = BuiltinId -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
    getBuiltinName' BuiltinId
    x
      go (PrimitiveName PrimitiveId
    x) = PrimitiveId -> m (Maybe QName)
    forall (m :: * -> *).
    HasBuiltins m =>
    PrimitiveId -> m (Maybe QName)
    getPrimitiveName' PrimitiveId
    x

    -- | @getTerm use name@ looks up @name@ as a primitive or builtin, and
    -- throws an error otherwise.
    -- The @use@ argument describes how the name is used for the sake of
    -- the error message.
    getTerm :: (HasBuiltins m, IsBuiltin a) => String -> a -> m Term
    getTerm :: forall (m :: * -> *) a.
    (HasBuiltins m, IsBuiltin a) =>
    String -> a -> m Term
    getTerm String
    use a
    name = (m Term -> m (Maybe Term) -> m Term)
    -> m (Maybe Term) -> m Term -> m Term
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip m Term -> m (Maybe Term) -> m Term
    forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
    fromMaybeM (a -> m (Maybe Term)
    forall (m :: * -> *) a.
    (HasBuiltins m, IsBuiltin a) =>
    a -> m (Maybe Term)
    getTerm' a
    name) (m Term -> m Term) -> m Term -> m Term
    forall a b. (a -> b) -> a -> b
    $
      Term -> m Term
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> m Term) -> Term -> m Term
    forall a b. (a -> b) -> a -> b
    $! Impossible -> Term
    forall a. Impossible -> a
    throwImpossible ([String] -> String -> Impossible
    ImpMissingDefinitions [a -> String
    forall a. IsBuiltin a => a -> String
    getBuiltinId a
    name] String
    use)

    -- | Rewrite a literal to constructor form if possible.
    constructorForm :: HasBuiltins m => Term -> m Term
    constructorForm :: forall (m :: * -> *). HasBuiltins m => Term -> m Term
    constructorForm Term
    v = do
      let pZero :: m Term
    pZero = Term -> Maybe Term -> Term
    forall a. a -> Maybe a -> a
    fromMaybe Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> BuiltinId -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinZero
          pSuc :: m Term
    pSuc  = Term -> Maybe Term -> Term
    forall a. a -> Maybe a -> a
    fromMaybe Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> BuiltinId -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinSuc
      m Term -> m Term -> Term -> m Term
    forall (m :: * -> *).
    Applicative m =>
    m Term -> m Term -> Term -> m Term
    constructorForm' m Term
    pZero m Term
    pSuc Term
    v

    {-# INLINABLE constructorForm' #-}
    {-# SPECIALIZE constructorForm' :: TCM Term -> TCM Term -> Term -> TCM Term #-}
    constructorForm' :: Applicative m => m Term -> m Term -> Term -> m Term
    constructorForm' :: forall (m :: * -> *).
    Applicative m =>
    m Term -> m Term -> Term -> m Term
    constructorForm' m Term
    pZero m Term
    pSuc Term
    v =
      case Term
    v of
        Lit (LitNat Integer
    n)
          | Integer
    n Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0    -> m Term
    pZero
          | Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    0     -> (Term -> KillRangeT Term
    forall t. Apply t => t -> Term -> t
    `apply1` Literal -> Term
    Lit (Integer -> Literal
    LitNat (Integer -> Literal) -> Integer -> Literal
    forall a b. (a -> b) -> a -> b
    $ Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1)) KillRangeT Term -> m Term -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Term
    pSuc
          | Bool
    otherwise -> Term -> m Term
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    v
        Term
    _ -> Term -> m Term
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    v

    ---------------------------------------------------------------------------
    -- * The names of built-in things
    ---------------------------------------------------------------------------

    primInteger, primIntegerPos, primIntegerNegSuc,
        primFloat, primChar, primString, primUnit, primUnitUnit, primBool, primTrue, primFalse,
        primSigma,
        primList, primNil, primCons, primIO, primNat, primSuc, primZero, primMaybe, primNothing, primJust,
        primPath, primPathP, primIntervalUniv, primInterval, primIZero, primIOne, primPartial, primPartialP,
        primIMin, primIMax, primINeg,
        primIsOne, primItIsOne, primIsOne1, primIsOne2, primIsOneEmpty,
        primSub, primSubIn, primSubOut,
        primTrans, primHComp,
        primEquiv, primEquivFun, primEquivProof,
        primTranspProof,
        primGlue, prim_glue, prim_unglue,
        prim_glueU, prim_unglueU,
        primFaceForall,
        primNatPlus, primNatMinus, primNatTimes, primNatDivSucAux, primNatModSucAux,
        primNatEquality, primNatLess,
        -- Machine words
        primWord64,
        primSizeUniv, primSize, primSizeLt, primSizeSuc, primSizeInf, primSizeMax,
        primInf, primSharp, primFlat,
        primEquality, primRefl,
        primLevel, primLevelZero, primLevelSuc, primLevelMax,
        primLockUniv,
        primLevelUniv,
        primProp, primSet, primStrictSet, primPropOmega, primSetOmega, primSSetOmega,
        primFromNat, primFromNeg, primFromString,
        -- builtins for reflection:
        primQName, primArgInfo, primArgArgInfo, primArg, primArgArg, primAbs, primAbsAbs, primAgdaTerm, primAgdaTermVar,
        primAgdaTermLam, primAgdaTermExtLam, primAgdaTermDef, primAgdaTermCon, primAgdaTermPi,
        primAgdaTermSort, primAgdaTermLit, primAgdaTermUnsupported, primAgdaTermMeta,
        primAgdaErrorPart, primAgdaErrorPartString, primAgdaErrorPartTerm, primAgdaErrorPartPatt, primAgdaErrorPartName,
        primHiding, primHidden, primInstance, primVisible,
        primRelevance, primRelevant, primIrrelevant,
        primQuantity, primQuantity0, primQuantityω,
        primModality, primModalityConstructor,
        primAssoc, primAssocLeft, primAssocRight, primAssocNon,
        primPrecedence, primPrecRelated, primPrecUnrelated,
        primFixity, primFixityFixity,
        primAgdaLiteral, primAgdaLitNat, primAgdaLitWord64, primAgdaLitFloat, primAgdaLitString, primAgdaLitChar, primAgdaLitQName, primAgdaLitMeta,
        primAgdaSort, primAgdaSortSet, primAgdaSortLit, primAgdaSortProp, primAgdaSortPropLit, primAgdaSortInf, primAgdaSortUnsupported,
        primAgdaDefinition, primAgdaDefinitionFunDef, primAgdaDefinitionDataDef, primAgdaDefinitionRecordDef,
        primAgdaDefinitionPostulate, primAgdaDefinitionPrimitive, primAgdaDefinitionDataConstructor,
        primAgdaClause, primAgdaClauseClause, primAgdaClauseAbsurd,
        primAgdaPattern, primAgdaPatCon, primAgdaPatVar, primAgdaPatDot,
        primAgdaPatLit, primAgdaPatProj,
        primAgdaPatAbsurd,
        primAgdaMeta,
        primAgdaBlocker, primAgdaBlockerAny, primAgdaBlockerAll, primAgdaBlockerMeta,
        primAgdaTCM, primAgdaTCMReturn, primAgdaTCMBind, primAgdaTCMUnify,
        primAgdaTCMTypeError, primAgdaTCMInferType, primAgdaTCMCheckType,
        primAgdaTCMNormalise, primAgdaTCMReduce,
        primAgdaTCMCatchError, primAgdaTCMGetContext, primAgdaTCMExtendContext, primAgdaTCMInContext,
        primAgdaTCMFreshName, primAgdaTCMDeclareDef, primAgdaTCMDeclarePostulate, primAgdaTCMDeclareData, primAgdaTCMDefineData, primAgdaTCMDefineFun,
        primAgdaTCMGetType, primAgdaTCMGetDefinition,
        primAgdaTCMQuoteTerm, primAgdaTCMUnquoteTerm, primAgdaTCMQuoteOmegaTerm,
        primAgdaTCMCommit, primAgdaTCMIsMacro, primAgdaTCMBlock,
        primAgdaTCMFormatErrorParts, primAgdaTCMDebugPrint,
        primAgdaTCMWithNormalisation, primAgdaTCMWithReconstructed,
        primAgdaTCMWithExpandLast, primAgdaTCMWithReduceDefs,
        primAgdaTCMAskNormalisation, primAgdaTCMAskReconstructed,
        primAgdaTCMAskExpandLast, primAgdaTCMAskReduceDefs,
        primAgdaTCMNoConstraints,
        primAgdaTCMWorkOnTypes,
        primAgdaTCMRunSpeculative,
        primAgdaTCMExec,
        primAgdaTCMCheckFromString,
        primAgdaTCMGetInstances,
        primAgdaTCMSolveInstances,
        primAgdaTCMPragmaForeign,
        primAgdaTCMPragmaCompile
        :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

    primInteger :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primInteger                           = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinInteger
    primIntegerPos :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIntegerPos                        = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinIntegerPos
    primIntegerNegSuc :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIntegerNegSuc                     = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinIntegerNegSuc
    primFloat :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primFloat                             = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinFloat
    primChar :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primChar                              = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinChar
    primString :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primString                            = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinString
    primBool :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primBool                              = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinBool
    primSigma :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSigma                             = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinSigma
    primUnit :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primUnit                              = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinUnit
    primUnitUnit :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primUnitUnit                          = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinUnitUnit
    primTrue :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primTrue                              = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinTrue
    primFalse :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primFalse                             = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinFalse
    primList :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primList                              = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinList
    primNil :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primNil                               = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinNil
    primCons :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primCons                              = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinCons
    primMaybe :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primMaybe                             = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinMaybe
    primNothing :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primNothing                           = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinNothing
    primJust :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primJust                              = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinJust
    primIO :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIO                                = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinIO
    primPath :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primPath                              = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinPath
    primPathP :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primPathP                             = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinPathP
    primIntervalUniv :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIntervalUniv                      = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinIntervalUniv
    primInterval :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primInterval                          = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinInterval
    primIZero :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIZero                             = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinIZero
    primIOne :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIOne                              = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinIOne
    primIMin :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIMin                              = PrimitiveId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    PrimitiveId -> m Term
    getPrimitiveTerm PrimitiveId
    builtinIMin
    primIMax :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIMax                              = PrimitiveId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    PrimitiveId -> m Term
    getPrimitiveTerm PrimitiveId
    builtinIMax
    primINeg :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primINeg                              = PrimitiveId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    PrimitiveId -> m Term
    getPrimitiveTerm PrimitiveId
    builtinINeg
    primPartial :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primPartial                           = PrimitiveId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    PrimitiveId -> m Term
    getPrimitiveTerm PrimitiveId
    PrimPartial
    primPartialP :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primPartialP                          = PrimitiveId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    PrimitiveId -> m Term
    getPrimitiveTerm PrimitiveId
    PrimPartialP
    primIsOne :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIsOne                             = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinIsOne
    primItIsOne :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primItIsOne                           = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinItIsOne
    primTrans :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primTrans                             = PrimitiveId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    PrimitiveId -> m Term
    getPrimitiveTerm PrimitiveId
    builtinTrans
    primHComp :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primHComp                             = PrimitiveId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    PrimitiveId -> m Term
    getPrimitiveTerm PrimitiveId
    builtinHComp
    primEquiv :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primEquiv                             = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinEquiv
    primEquivFun :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primEquivFun                          = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinEquivFun
    primEquivProof :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primEquivProof                        = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinEquivProof
    primTranspProof :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primTranspProof                       = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinTranspProof
    prim_glueU :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    prim_glueU                            = PrimitiveId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    PrimitiveId -> m Term
    getPrimitiveTerm PrimitiveId
    builtin_glueU
    prim_unglueU :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    prim_unglueU                          = PrimitiveId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    PrimitiveId -> m Term
    getPrimitiveTerm PrimitiveId
    builtin_unglueU
    primGlue :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primGlue                              = PrimitiveId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    PrimitiveId -> m Term
    getPrimitiveTerm PrimitiveId
    builtinGlue
    prim_glue :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    prim_glue                             = PrimitiveId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    PrimitiveId -> m Term
    getPrimitiveTerm PrimitiveId
    builtin_glue
    prim_unglue :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    prim_unglue                           = PrimitiveId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    PrimitiveId -> m Term
    getPrimitiveTerm PrimitiveId
    builtin_unglue
    primFaceForall :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primFaceForall                        = PrimitiveId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    PrimitiveId -> m Term
    getPrimitiveTerm PrimitiveId
    builtinFaceForall
    primIsOne1 :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIsOne1                            = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinIsOne1
    primIsOne2 :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIsOne2                            = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinIsOne2
    primIsOneEmpty :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIsOneEmpty                        = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinIsOneEmpty
    primSub :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSub                               = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinSub
    primSubIn :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSubIn                             = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinSubIn
    primSubOut :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSubOut                            = PrimitiveId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    PrimitiveId -> m Term
    getPrimitiveTerm PrimitiveId
    builtinSubOut
    primNat :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primNat                               = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinNat
    primSuc :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSuc                               = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinSuc
    primZero :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primZero                              = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinZero
    primNatPlus :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primNatPlus                           = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinNatPlus
    primNatMinus :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primNatMinus                          = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinNatMinus
    primNatTimes :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primNatTimes                          = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinNatTimes
    primNatDivSucAux :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primNatDivSucAux                      = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinNatDivSucAux
    primNatModSucAux :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primNatModSucAux                      = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinNatModSucAux
    primNatEquality :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primNatEquality                       = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinNatEquals
    primNatLess :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primNatLess                           = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinNatLess
    primWord64 :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primWord64                            = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinWord64
    primSizeUniv :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSizeUniv                          = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinSizeUniv
    primSize :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSize                              = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinSize
    primSizeLt :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSizeLt                            = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinSizeLt
    primSizeSuc :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSizeSuc                           = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinSizeSuc
    primSizeInf :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSizeInf                           = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinSizeInf
    primSizeMax :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSizeMax                           = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinSizeMax
    primInf :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primInf                               = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinInf
    primSharp :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSharp                             = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinSharp
    primFlat :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primFlat                              = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinFlat
    primEquality :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primEquality                          = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinEquality
    primRefl :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primRefl                              = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinRefl
    primLevel :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primLevel                             = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinLevel
    primLevelZero :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primLevelZero                         = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinLevelZero
    primLevelSuc :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primLevelSuc                          = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinLevelSuc
    primLevelMax :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primLevelMax                          = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinLevelMax
    primProp :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primProp                              = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinProp
    primSet :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSet                               = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinSet
    primStrictSet :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primStrictSet                         = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinStrictSet
    primPropOmega :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primPropOmega                         = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinPropOmega
    primSetOmega :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSetOmega                          = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinSetOmega
    primSSetOmega :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSSetOmega                         = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinSSetOmega
    primLockUniv :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primLockUniv                          = PrimitiveId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    PrimitiveId -> m Term
    getPrimitiveTerm PrimitiveId
    builtinLockUniv
    primLevelUniv :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primLevelUniv                         = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinLevelUniv
    primFromNat :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primFromNat                           = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinFromNat
    primFromNeg :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primFromNeg                           = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinFromNeg
    primFromString :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primFromString                        = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinFromString
    primQName :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primQName                             = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinQName
    primArg :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primArg                               = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinArg
    primArgArg :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primArgArg                            = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinArgArg
    primAbs :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAbs                               = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAbs
    primAbsAbs :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAbsAbs                            = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAbsAbs
    primAgdaSort :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaSort                          = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaSort
    primHiding :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primHiding                            = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinHiding
    primHidden :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primHidden                            = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinHidden
    primInstance :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primInstance                          = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinInstance
    primVisible :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primVisible                           = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinVisible
    primRelevance :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primRelevance                         = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinRelevance
    primRelevant :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primRelevant                          = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinRelevant
    primIrrelevant :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIrrelevant                        = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinIrrelevant
    primQuantity :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primQuantity                          = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinQuantity
    primQuantity0 :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primQuantity0                         = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinQuantity0
    primQuantityω :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primQuantityω                         = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinQuantityω
    primModality :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primModality                          = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinModality
    primModalityConstructor :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primModalityConstructor               = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinModalityConstructor
    primAssoc :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAssoc                             = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAssoc
    primAssocLeft :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAssocLeft                         = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAssocLeft
    primAssocRight :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAssocRight                        = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAssocRight
    primAssocNon :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAssocNon                          = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAssocNon
    primPrecedence :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primPrecedence                        = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinPrecedence
    primPrecRelated :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primPrecRelated                       = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinPrecRelated
    primPrecUnrelated :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primPrecUnrelated                     = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinPrecUnrelated
    primFixity :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primFixity                            = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinFixity
    primFixityFixity :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primFixityFixity                      = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinFixityFixity
    primAgdaBlocker :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaBlocker                       = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaBlocker
    primAgdaBlockerAny :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaBlockerAny                    = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaBlockerAny
    primAgdaBlockerAll :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaBlockerAll                    = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaBlockerAll
    primAgdaBlockerMeta :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaBlockerMeta                   = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaBlockerMeta
    primArgInfo :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primArgInfo                           = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinArgInfo
    primArgArgInfo :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primArgArgInfo                        = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinArgArgInfo
    primAgdaSortSet :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaSortSet                       = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaSortSet
    primAgdaSortLit :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaSortLit                       = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaSortLit
    primAgdaSortProp :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaSortProp                      = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaSortProp
    primAgdaSortPropLit :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaSortPropLit                   = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaSortPropLit
    primAgdaSortInf :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaSortInf                       = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaSortInf
    primAgdaSortUnsupported :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaSortUnsupported               = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaSortUnsupported
    primAgdaTerm :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTerm                          = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTerm
    primAgdaTermVar :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTermVar                       = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTermVar
    primAgdaTermLam :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTermLam                       = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTermLam
    primAgdaTermExtLam :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTermExtLam                    = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTermExtLam
    primAgdaTermDef :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTermDef                       = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTermDef
    primAgdaTermCon :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTermCon                       = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTermCon
    primAgdaTermPi :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTermPi                        = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTermPi
    primAgdaTermSort :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTermSort                      = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTermSort
    primAgdaTermLit :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTermLit                       = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTermLit
    primAgdaTermUnsupported :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTermUnsupported               = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTermUnsupported
    primAgdaTermMeta :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTermMeta                      = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTermMeta
    primAgdaErrorPart :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaErrorPart                     = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaErrorPart
    primAgdaErrorPartString :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaErrorPartString               = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaErrorPartString
    primAgdaErrorPartTerm :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaErrorPartTerm                 = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaErrorPartTerm
    primAgdaErrorPartPatt :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaErrorPartPatt                 = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaErrorPartPatt
    primAgdaErrorPartName :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaErrorPartName                 = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaErrorPartName
    primAgdaLiteral :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaLiteral                       = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaLiteral
    primAgdaLitNat :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaLitNat                        = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaLitNat
    primAgdaLitWord64 :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaLitWord64                     = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaLitWord64
    primAgdaLitFloat :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaLitFloat                      = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaLitFloat
    primAgdaLitChar :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaLitChar                       = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaLitChar
    primAgdaLitString :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaLitString                     = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaLitString
    primAgdaLitQName :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaLitQName                      = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaLitQName
    primAgdaLitMeta :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaLitMeta                       = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaLitMeta
    primAgdaPattern :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaPattern                       = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaPattern
    primAgdaPatCon :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaPatCon                        = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaPatCon
    primAgdaPatVar :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaPatVar                        = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaPatVar
    primAgdaPatDot :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaPatDot                        = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaPatDot
    primAgdaPatLit :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaPatLit                        = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaPatLit
    primAgdaPatProj :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaPatProj                       = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaPatProj
    primAgdaPatAbsurd :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaPatAbsurd                     = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaPatAbsurd
    primAgdaClause :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaClause                        = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaClause
    primAgdaClauseClause :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaClauseClause                  = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaClauseClause
    primAgdaClauseAbsurd :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaClauseAbsurd                  = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaClauseAbsurd
    primAgdaDefinitionFunDef :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaDefinitionFunDef              = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaDefinitionFunDef
    primAgdaDefinitionDataDef :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaDefinitionDataDef             = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaDefinitionDataDef
    primAgdaDefinitionRecordDef :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaDefinitionRecordDef           = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaDefinitionRecordDef
    primAgdaDefinitionDataConstructor :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaDefinitionDataConstructor     = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaDefinitionDataConstructor
    primAgdaDefinitionPostulate :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaDefinitionPostulate           = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaDefinitionPostulate
    primAgdaDefinitionPrimitive :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaDefinitionPrimitive           = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaDefinitionPrimitive
    primAgdaDefinition :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaDefinition                    = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaDefinition
    primAgdaMeta :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaMeta                          = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaMeta
    primAgdaTCM :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCM                           = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCM
    primAgdaTCMReturn :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMReturn                     = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMReturn
    primAgdaTCMBind :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMBind                       = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMBind
    primAgdaTCMUnify :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMUnify                      = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMUnify
    primAgdaTCMTypeError :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMTypeError                  = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMTypeError
    primAgdaTCMInferType :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMInferType                  = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMInferType
    primAgdaTCMCheckType :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMCheckType                  = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMCheckType
    primAgdaTCMNormalise :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMNormalise                  = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMNormalise
    primAgdaTCMReduce :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMReduce                     = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMReduce
    primAgdaTCMCatchError :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMCatchError                 = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMCatchError
    primAgdaTCMGetContext :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMGetContext                 = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMGetContext
    primAgdaTCMExtendContext :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMExtendContext              = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMExtendContext
    primAgdaTCMInContext :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMInContext                  = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMInContext
    primAgdaTCMFreshName :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMFreshName                  = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMFreshName
    primAgdaTCMDeclareDef :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMDeclareDef                 = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMDeclareDef
    primAgdaTCMDeclarePostulate :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMDeclarePostulate           = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMDeclarePostulate
    primAgdaTCMDeclareData :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMDeclareData                = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMDeclareData
    primAgdaTCMDefineData :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMDefineData                 = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMDefineData
    primAgdaTCMDefineFun :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMDefineFun                  = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMDefineFun
    primAgdaTCMGetType :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMGetType                    = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMGetType
    primAgdaTCMGetDefinition :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMGetDefinition              = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMGetDefinition
    primAgdaTCMQuoteTerm :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMQuoteTerm                  = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMQuoteTerm
    primAgdaTCMQuoteOmegaTerm :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMQuoteOmegaTerm             = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMQuoteOmegaTerm
    primAgdaTCMUnquoteTerm :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMUnquoteTerm                = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMUnquoteTerm
    primAgdaTCMBlock :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMBlock                      = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMBlock
    primAgdaTCMCommit :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMCommit                     = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMCommit
    primAgdaTCMIsMacro :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMIsMacro                    = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMIsMacro
    primAgdaTCMWithNormalisation :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMWithNormalisation          = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMWithNormalisation
    primAgdaTCMWithReconstructed :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMWithReconstructed          = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMWithReconstructed
    primAgdaTCMWithExpandLast :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMWithExpandLast             = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMWithExpandLast
    primAgdaTCMWithReduceDefs :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMWithReduceDefs             = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMWithReduceDefs
    primAgdaTCMAskNormalisation :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMAskNormalisation           = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMAskNormalisation
    primAgdaTCMAskReconstructed :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMAskReconstructed           = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMAskReconstructed
    primAgdaTCMAskExpandLast :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMAskExpandLast              = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMAskExpandLast
    primAgdaTCMAskReduceDefs :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMAskReduceDefs              = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMAskReduceDefs
    primAgdaTCMFormatErrorParts :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMFormatErrorParts           = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMFormatErrorParts
    primAgdaTCMDebugPrint :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMDebugPrint                 = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMDebugPrint
    primAgdaTCMNoConstraints :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMNoConstraints              = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMNoConstraints
    primAgdaTCMWorkOnTypes :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMWorkOnTypes                = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMWorkOnTypes
    primAgdaTCMRunSpeculative :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMRunSpeculative             = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMRunSpeculative
    primAgdaTCMExec :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMExec                       = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMExec
    primAgdaTCMCheckFromString :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMCheckFromString            = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMCheckFromString
    primAgdaTCMGetInstances :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMGetInstances               = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMGetInstances
    primAgdaTCMSolveInstances :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMSolveInstances             = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMSolveInstances
    primAgdaTCMPragmaForeign :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMPragmaForeign              = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMPragmaForeign
    primAgdaTCMPragmaCompile :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCMPragmaCompile              = BuiltinId -> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m Term
    getBuiltin BuiltinId
    builtinAgdaTCMPragmaCompile

    -- | The coinductive primitives.

    data CoinductionKit = CoinductionKit
      { CoinductionKit -> QName
    nameOfInf   :: QName
      , CoinductionKit -> QName
    nameOfSharp :: QName
      , CoinductionKit -> QName
    nameOfFlat  :: QName
      }

    -- | Tries to build a 'CoinductionKit'.

    coinductionKit' :: TCM CoinductionKit
    coinductionKit' :: TCM CoinductionKit
    coinductionKit' = do
      inf   <- BuiltinId -> TCMT IO QName
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m QName
    getBuiltinName_ BuiltinId
    builtinInf
      sharp <- getBuiltinName_ builtinSharp
      flat  <- getBuiltinName_ builtinFlat
      return $ CoinductionKit
        { nameOfInf   = inf
        , nameOfSharp = sharp
        , nameOfFlat  = flat
        }

    coinductionKit :: TCM (Maybe CoinductionKit)
    coinductionKit :: TCM (Maybe CoinductionKit)
    coinductionKit = TCM CoinductionKit -> TCM (Maybe CoinductionKit)
    forall e (m :: * -> *) a.
    (MonadError e m, Functor m) =>
    m a -> m (Maybe a)
    tryMaybe TCM CoinductionKit
    coinductionKit'

    -- | Sort primitives.

    data SortKit = SortKit
      { SortKit -> UnivSize -> Univ -> QName
    nameOfUniv   :: UnivSize -> Univ -> QName
      , SortKit -> QName -> Maybe (UnivSize, Univ)
    isNameOfUniv :: QName -> Maybe (UnivSize, Univ)
      }

    mkSortKit :: QName -> QName -> QName -> QName -> QName -> QName -> SortKit
    mkSortKit :: QName -> QName -> QName -> QName -> QName -> QName -> SortKit
    mkSortKit QName
    prop QName
    set QName
    sset QName
    propomega QName
    setomega QName
    ssetomega = SortKit
      { nameOfUniv :: UnivSize -> Univ -> QName
    nameOfUniv = ((UnivSize, Univ) -> QName) -> UnivSize -> Univ -> QName
    forall a b c. ((a, b) -> c) -> a -> b -> c
    curry (((UnivSize, Univ) -> QName) -> UnivSize -> Univ -> QName)
    -> ((UnivSize, Univ) -> QName) -> UnivSize -> Univ -> QName
    forall a b. (a -> b) -> a -> b
    $ \case
          (UnivSize
    USmall , Univ
    UProp) -> QName
    prop
          (UnivSize
    USmall , Univ
    UType) -> QName
    set
          (UnivSize
    USmall , Univ
    USSet) -> QName
    sset
          (UnivSize
    ULarge , Univ
    UProp) -> QName
    propomega
          (UnivSize
    ULarge , Univ
    UType) -> QName
    setomega
          (UnivSize
    ULarge , Univ
    USSet) -> QName
    ssetomega
      , isNameOfUniv :: QName -> Maybe (UnivSize, Univ)
    isNameOfUniv = \ QName
    x -> if
          | QName
    x QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    prop      -> (UnivSize, Univ) -> Maybe (UnivSize, Univ)
    forall a. a -> Maybe a
    Just (UnivSize
    USmall , Univ
    UProp)
          | QName
    x QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    set       -> (UnivSize, Univ) -> Maybe (UnivSize, Univ)
    forall a. a -> Maybe a
    Just (UnivSize
    USmall , Univ
    UType)
          | QName
    x QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    sset      -> (UnivSize, Univ) -> Maybe (UnivSize, Univ)
    forall a. a -> Maybe a
    Just (UnivSize
    USmall , Univ
    USSet)
          | QName
    x QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    propomega -> (UnivSize, Univ) -> Maybe (UnivSize, Univ)
    forall a. a -> Maybe a
    Just (UnivSize
    ULarge , Univ
    UProp)
          | QName
    x QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    setomega  -> (UnivSize, Univ) -> Maybe (UnivSize, Univ)
    forall a. a -> Maybe a
    Just (UnivSize
    ULarge , Univ
    UType)
          | QName
    x QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    ssetomega -> (UnivSize, Univ) -> Maybe (UnivSize, Univ)
    forall a. a -> Maybe a
    Just (UnivSize
    ULarge , Univ
    USSet)
          | Bool
    otherwise -> Maybe (UnivSize, Univ)
    forall a. Maybe a
    Nothing
      }

    -- | Compute a 'SortKit' in an environment that supports failures.
    --
    -- When 'optLoadPrimitives' is set to 'False', 'sortKit' is a fallible operation,
    -- so for the uses of 'sortKit' in fallible contexts (e.g. 'TCM'),
    -- we report a type error rather than exploding.
    sortKit :: (HasBuiltins m, MonadTCError m, HasOptions m) => m SortKit
    sortKit :: forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m, HasOptions m) =>
    m SortKit
    sortKit = do
      prop      <- BuiltinId -> m QName
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m QName
    getBuiltinName_ BuiltinId
    builtinProp
      set       <- getBuiltinName_ builtinSet
      sset      <- getBuiltinName_ builtinStrictSet
      propomega <- getBuiltinName_ builtinPropOmega
      setomega  <- getBuiltinName_ builtinSetOmega
      ssetomega <- getBuiltinName_ builtinSSetOmega
      return $ mkSortKit prop set sset propomega setomega ssetomega

    -- | Compute a 'SortKit' in contexts that do not support failure (e.g.
    -- 'Reify'). This should only be used when we are sure that the
    -- primitive sorts have been bound, i.e. because it is "after" type
    -- checking.
    infallibleSortKit :: HasBuiltins m => m SortKit
    infallibleSortKit :: forall (m :: * -> *). HasBuiltins m => m SortKit
    infallibleSortKit = do
      prop      <- QName -> Maybe QName -> QName
    forall a. a -> Maybe a -> a
    fromMaybe QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe QName -> QName) -> m (Maybe QName) -> m QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> BuiltinId -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
    getBuiltinName' BuiltinId
    builtinProp
      set       <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinSet
      sset      <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinStrictSet
      propomega <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinPropOmega
      setomega  <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinSetOmega
      ssetomega <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinSSetOmega
      return $ mkSortKit prop set sset propomega setomega ssetomega

    ------------------------------------------------------------------------
    -- * Path equality
    ------------------------------------------------------------------------

    getPrimName :: Term -> QName
    getPrimName :: Term -> QName
    getPrimName Term
    ty = do
      let lamV :: Term -> ([Hiding], Term)
    lamV (Lam ArgInfo
    i Abs Term
    b)  = ([Hiding] -> [Hiding]) -> ([Hiding], Term) -> ([Hiding], Term)
    forall a c b. (a -> c) -> (a, b) -> (c, b)
    mapFst (ArgInfo -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding ArgInfo
    i Hiding -> [Hiding] -> [Hiding]
    forall a. a -> [a] -> [a]
    :) (([Hiding], Term) -> ([Hiding], Term))
    -> ([Hiding], Term) -> ([Hiding], Term)
    forall a b. (a -> b) -> a -> b
    $ Term -> ([Hiding], Term)
    lamV (Abs Term -> Term
    forall a. Abs a -> a
    unAbs Abs Term
    b)
          lamV (Pi Dom Type
    _ Abs Type
    b)   = Term -> ([Hiding], Term)
    lamV (Type -> Term
    forall t a. Type'' t a -> a
    unEl (Type -> Term) -> Type -> Term
    forall a b. (a -> b) -> a -> b
    $ Abs Type -> Type
    forall a. Abs a -> a
    unAbs Abs Type
    b)
          lamV Term
    v          = ([], Term
    v)
      case Term -> ([Hiding], Term)
    lamV Term
    ty of
                ([Hiding]
    _, Def QName
    path Elims
    _) -> QName
    path
                ([Hiding]
    _, Con ConHead
    nm ConInfo
    _ Elims
    _)   -> ConHead -> QName
    conName ConHead
    nm
                ([Hiding]
    _, Var Int
    0 [Proj ProjOrigin
    _ QName
    l]) -> QName
    l
                ([Hiding]
    _, Term
    t)          -> QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    getBuiltinName' :: HasBuiltins m => BuiltinId -> m (Maybe QName)
    getBuiltinName' :: forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
    getBuiltinName' BuiltinId
    n = (Term -> QName) -> Maybe Term -> Maybe QName
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Term -> QName
    getPrimName (Maybe Term -> Maybe QName) -> m (Maybe Term) -> m (Maybe QName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> BuiltinId -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    n

    getPrimitiveName' :: HasBuiltins m => PrimitiveId -> m (Maybe QName)
    getPrimitiveName' :: forall (m :: * -> *).
    HasBuiltins m =>
    PrimitiveId -> m (Maybe QName)
    getPrimitiveName' PrimitiveId
    n = (PrimFun -> QName) -> Maybe PrimFun -> Maybe QName
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap PrimFun -> QName
    primFunName (Maybe PrimFun -> Maybe QName)
    -> m (Maybe PrimFun) -> m (Maybe QName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PrimitiveId -> m (Maybe PrimFun)
    forall (m :: * -> *).
    HasBuiltins m =>
    PrimitiveId -> m (Maybe PrimFun)
    getPrimitive' PrimitiveId
    n

    isPrimitive :: HasBuiltins m => PrimitiveId -> QName -> m Bool
    isPrimitive :: forall (m :: * -> *).
    HasBuiltins m =>
    PrimitiveId -> QName -> m Bool
    isPrimitive PrimitiveId
    n QName
    q = (QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    q Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Maybe QName -> Bool) -> m (Maybe QName) -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PrimitiveId -> m (Maybe QName)
    forall (m :: * -> *).
    HasBuiltins m =>
    PrimitiveId -> m (Maybe QName)
    getPrimitiveName' PrimitiveId
    n

    intervalSort :: Sort
    intervalSort :: Sort' Term
    intervalSort = Sort' Term
    forall t. Sort' t
    IntervalUniv

    {-# SPECIALIZE intervalView' :: TCM (Term -> IntervalView) #-}
    {-# INLINABLE intervalView' #-}
    intervalView' :: HasBuiltins m => m (Term -> IntervalView)
    intervalView' :: forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
    intervalView' = do
      iz <- BuiltinId -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
    getBuiltinName' BuiltinId
    builtinIZero
      io <- getBuiltinName' builtinIOne
      imax <- getPrimitiveName' builtinIMax
      imin <- getPrimitiveName' builtinIMin
      ineg <- getPrimitiveName' builtinINeg
      return $ \ Term
    t ->
        case Term
    t of
          Def QName
    q Elims
    es ->
            case Elims
    es of
              [Apply Arg Term
    x,Apply Arg Term
    y] | QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    q Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    imin -> Arg Term -> Arg Term -> IntervalView
    IMin Arg Term
    x Arg Term
    y
              [Apply Arg Term
    x,Apply Arg Term
    y] | QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    q Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    imax -> Arg Term -> Arg Term -> IntervalView
    IMax Arg Term
    x Arg Term
    y
              [Apply Arg Term
    x]         | QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    q Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    ineg -> Arg Term -> IntervalView
    INeg Arg Term
    x
              Elims
    _                 -> Term -> IntervalView
    OTerm Term
    t
          Con ConHead
    q ConInfo
    _ [] | QName -> Maybe QName
    forall a. a -> Maybe a
    Just (ConHead -> QName
    conName ConHead
    q) Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    iz -> IntervalView
    IZero
                     | QName -> Maybe QName
    forall a. a -> Maybe a
    Just (ConHead -> QName
    conName ConHead
    q) Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    io -> IntervalView
    IOne
          Term
    _ -> Term -> IntervalView
    OTerm Term
    t

    {-# INLINE intervalView #-}
    intervalView :: HasBuiltins m => Term -> m IntervalView
    intervalView :: forall (m :: * -> *). HasBuiltins m => Term -> m IntervalView
    intervalView Term
    t = do
      f <- m (Term -> IntervalView)
    forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
    intervalView'
      return (f t)

    intervalUnview :: HasBuiltins m => IntervalView -> m Term
    intervalUnview :: forall (m :: * -> *). HasBuiltins m => IntervalView -> m Term
    intervalUnview IntervalView
    t = do
      f <- m (IntervalView -> Term)
    forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
    intervalUnview'
      return (f t)

    {-# SPECIALIZE intervalUnview' :: TCM (IntervalView -> Term) #-}
    intervalUnview' :: HasBuiltins m => m (IntervalView -> Term)
    intervalUnview' :: forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
    intervalUnview' = do
      iz <- Term -> Maybe Term -> Term
    forall a. a -> Maybe a -> a
    fromMaybe Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> BuiltinId -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinIZero -- should it be a type error instead?
      io <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinIOne
      imin <- (`Def` []) . fromMaybe __IMPOSSIBLE__ <$> getPrimitiveName' builtinIMin
      imax <- (`Def` []) . fromMaybe __IMPOSSIBLE__ <$> getPrimitiveName' builtinIMax
      ineg <- (`Def` []) . fromMaybe __IMPOSSIBLE__ <$> getPrimitiveName' builtinINeg
      return $ \ IntervalView
    v -> case IntervalView
    v of
                 IntervalView
    IZero -> Term
    iz
                 IntervalView
    IOne  -> Term
    io
                 IMin Arg Term
    x Arg Term
    y -> Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    apply Term
    imin [Arg Term
    x,Arg Term
    y]
                 IMax Arg Term
    x Arg Term
    y -> Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    apply Term
    imax [Arg Term
    x,Arg Term
    y]
                 INeg Arg Term
    x   -> Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    apply Term
    ineg [Arg Term
    x]
                 OTerm Term
    t -> Term
    t

    ------------------------------------------------------------------------
    -- * Path equality
    ------------------------------------------------------------------------

    -- | Check whether the type is actually an path (lhs ≡ rhs)
    --   and extract lhs, rhs, and their type.
    --
    --   Precondition: type is reduced.

    {-# INLINE pathView #-}
    pathView :: HasBuiltins m => Type -> m PathView
    pathView :: forall (m :: * -> *). HasBuiltins m => Type -> m PathView
    pathView Type
    t0 = do
      view <- m (Type -> PathView)
    forall (m :: * -> *). HasBuiltins m => m (Type -> PathView)
    pathView'
      return $ view t0

    {-# SPECIALIZE pathView' :: TCM (Type -> PathView)  #-}
    pathView' :: HasBuiltins m => m (Type -> PathView)
    pathView' :: forall (m :: * -> *). HasBuiltins m => m (Type -> PathView)
    pathView' = do
     mpath  <- BuiltinId -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
    getBuiltinName' BuiltinId
    builtinPath
     mpathp <- getBuiltinName' builtinPathP
     return $ \ t0 :: Type
    t0@(El Sort' Term
    s Term
    t) ->
      case Term
    t of
        Def QName
    path' [ Apply Arg Term
    level , Apply Arg Term
    typ , Apply Arg Term
    lhs , Apply Arg Term
    rhs ]
          | QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    path' Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    mpath, Just QName
    path <- Maybe QName
    mpathp -> Sort' Term
    -> QName
    -> Arg Term
    -> Arg Term
    -> Arg Term
    -> Arg Term
    -> PathView
    PathType Sort' Term
    s QName
    path Arg Term
    level (KillRangeT Term
    lam_i KillRangeT Term -> Arg Term -> Arg Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term
    typ) Arg Term
    lhs Arg Term
    rhs
          where lam_i :: KillRangeT Term
    lam_i = ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    defaultArgInfo (Abs Term -> Term) -> (Term -> Abs Term) -> KillRangeT Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Term -> Abs Term
    forall a. String -> a -> Abs a
    NoAbs String
    "_"
        Def QName
    path' [ Apply Arg Term
    level , Apply Arg Term
    typ , Apply Arg Term
    lhs , Apply Arg Term
    rhs ]
          | QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    path' Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    mpathp, Just QName
    path <- Maybe QName
    mpathp -> Sort' Term
    -> QName
    -> Arg Term
    -> Arg Term
    -> Arg Term
    -> Arg Term
    -> PathView
    PathType Sort' Term
    s QName
    path Arg Term
    level Arg Term
    typ Arg Term
    lhs Arg Term
    rhs
        Term
    _ -> Type -> PathView
    OType Type
    t0

    boldPathView :: Type -> PathView
    boldPathView :: Type -> PathView
    boldPathView t0 :: Type
    t0@(El Sort' Term
    s Term
    t) = do
      case Term
    t of
        Def QName
    path' [ Apply Arg Term
    level , Apply Arg Term
    typ , Apply Arg Term
    lhs , Apply Arg Term
    rhs ]
          -> Sort' Term
    -> QName
    -> Arg Term
    -> Arg Term
    -> Arg Term
    -> Arg Term
    -> PathView
    PathType Sort' Term
    s QName
    path' Arg Term
    level Arg Term
    typ Arg Term
    lhs Arg Term
    rhs
        Term
    _ -> Type -> PathView
    OType Type
    t0

    -- | Revert the 'PathView'.
    --
    --   Postcondition: type is reduced.

    pathUnview :: PathView -> Type
    pathUnview :: PathView -> Type
    pathUnview (OType Type
    t) = Type
    t
    pathUnview (PathType Sort' Term
    s QName
    path Arg Term
    l Arg Term
    t Arg Term
    lhs Arg Term
    rhs) =
      Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort' Term
    s (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> Term
    Def QName
    path (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Elim' Term) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply [Arg Term
    l, Arg Term
    t, Arg Term
    lhs, Arg Term
    rhs]

    ------------------------------------------------------------------------
    -- * Builtin equality
    ------------------------------------------------------------------------

    -- | Get the name of the equality type.
    primEqualityName :: TCM QName
    primEqualityName :: TCMT IO QName
    primEqualityName = do
      eq <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primEquality
      -- Andreas, 2014-05-17 moved this here from TC.Rules.Def
      -- Don't know why up to 2 hidden lambdas need to be stripped,
      -- but I left the code in place.
      -- Maybe it was intended that equality could be declared
      -- in three different ways:
      -- 1. universe and type polymorphic
      -- 2. type polymorphic only
      -- 3. monomorphic.
      let lamV (Lam ArgInfo
    i Abs Term
    b)  = ([Hiding] -> [Hiding]) -> ([Hiding], Term) -> ([Hiding], Term)
    forall a c b. (a -> c) -> (a, b) -> (c, b)
    mapFst (ArgInfo -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding ArgInfo
    i Hiding -> [Hiding] -> [Hiding]
    forall a. a -> [a] -> [a]
    :) (([Hiding], Term) -> ([Hiding], Term))
    -> ([Hiding], Term) -> ([Hiding], Term)
    forall a b. (a -> b) -> a -> b
    $ Term -> ([Hiding], Term)
    lamV (Abs Term -> Term
    forall a. Abs a -> a
    unAbs Abs Term
    b)
          lamV Term
    v          = ([], Term
    v)
      return $ case lamV eq of
        ([Hiding]
    _, Def QName
    equality Elims
    _) -> QName
    equality
        ([Hiding], Term)
    _                   -> QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Check whether the type is actually an equality (lhs ≡ rhs)
    --   and extract lhs, rhs, and their type.
    --
    --   Precondition: type is reduced.

    equalityView ::
         Range  -- ^ Range of the @rewrite@ expression, if any.
      -> Type   -- ^ Identity type?
      -> TCM EqualityView
    equalityView :: Range -> Type -> TCM EqualityView
    equalityView Range
    r t0 :: Type
    t0@(El Sort' Term
    s Term
    t) = do
      equality <- TCMT IO QName
    primEqualityName
      case t of
        Def QName
    equality' Elims
    es | QName
    equality' QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    equality -> do
          let vs :: Args
    vs = Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es
          let n :: Int
    n = Args -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Args
    vs
          Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    3) TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          let (Args
    pars, [ Arg Term
    typ , Arg Term
    lhs, Arg Term
    rhs ]) = Int -> Args -> (Args, Args)
    forall a. Int -> [a] -> ([a], [a])
    splitAt (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    3) Args
    vs
          EqualityView -> TCM EqualityView
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (EqualityView -> TCM EqualityView)
    -> EqualityView -> TCM EqualityView
    forall a b. (a -> b) -> a -> b
    $ Range
    -> Sort' Term
    -> QName
    -> Args
    -> Arg Term
    -> Arg Term
    -> Arg Term
    -> EqualityView
    EqualityType Range
    r Sort' Term
    s QName
    equality Args
    pars Arg Term
    typ Arg Term
    lhs Arg Term
    rhs
        Term
    _ -> EqualityView -> TCM EqualityView
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (EqualityView -> TCM EqualityView)
    -> EqualityView -> TCM EqualityView
    forall a b. (a -> b) -> a -> b
    $ Type -> EqualityView
    OtherType Type
    t0

    -- | Revert the 'EqualityView'.
    --
    --   Postcondition: type is reduced.

    class EqualityUnview a where
      equalityUnview :: a -> Type

    instance EqualityUnview EqualityView where
      equalityUnview :: EqualityView -> Type
    equalityUnview = \case
        OtherType Type
    t -> Type
    t
        IdiomType Type
    t -> Type
    t
        EqualityViewType EqualityTypeData
    eqt -> EqualityTypeData -> Type
    forall a. EqualityUnview a => a -> Type
    equalityUnview EqualityTypeData
    eqt

    instance EqualityUnview EqualityTypeData where
      equalityUnview :: EqualityTypeData -> Type
    equalityUnview (EqualityTypeData Range
    _r Sort' Term
    s QName
    equality Args
    l Arg Term
    t Arg Term
    lhs Arg Term
    rhs) =
        Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort' Term
    s (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> Term
    Def QName
    equality (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Elim' Term) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Args
    l Args -> Args -> Args
    forall a. [a] -> [a] -> [a]
    ++ [Arg Term
    t, Arg Term
    lhs, Arg Term
    rhs])

    -- | Primitives with typechecking constrants.
    constrainedPrims :: [PrimitiveId]
    constrainedPrims :: [PrimitiveId]
    constrainedPrims =
      [ PrimitiveId
    builtinPOr
      , PrimitiveId
    builtinComp
      , PrimitiveId
    builtinHComp
      , PrimitiveId
    builtinTrans
      , PrimitiveId
    builtin_glue
      , PrimitiveId
    builtin_glueU
      ]

    getNameOfConstrained :: HasBuiltins m => PrimitiveId -> m (Maybe QName)
    getNameOfConstrained :: forall (m :: * -> *).
    HasBuiltins m =>
    PrimitiveId -> m (Maybe QName)
    getNameOfConstrained PrimitiveId
    s = do
      Bool -> m () -> m ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (PrimitiveId
    s PrimitiveId -> [PrimitiveId] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [PrimitiveId]
    constrainedPrims) m ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      PrimitiveId -> m (Maybe QName)
    forall (m :: * -> *) a.
    (HasBuiltins m, IsBuiltin a) =>
    a -> m (Maybe QName)
    getName' PrimitiveId
    s