Agda
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Monad.Builtin

Synopsis

Documentation

bindBuiltinName :: BuiltinId -> Term -> TCM () Source #

bindBuiltinRewriteRelation :: QName -> TCM () Source #

Add one (more) relation symbol to the rewrite relations.

bindPrimitive :: PrimitiveId -> PrimFun -> TCM () Source #

boldPathView :: Type -> PathView Source #

coinductionKit :: TCM (Maybe CoinductionKit) Source #

coinductionKit' :: TCM CoinductionKit Source #

Tries to build a CoinductionKit.

constrainedPrims :: [PrimitiveId] Source #

Primitives with typechecking constrants.

constructorForm :: HasBuiltins m => Term -> m Term Source #

Rewrite a literal to constructor form if possible.

constructorForm' :: Applicative m => m Term -> m Term -> Term -> m Term Source #

equalityView :: Type -> TCM EqualityView Source #

Check whether the type is actually an equality (lhs ≡ rhs) and extract lhs, rhs, and their type.

Precondition: type is reduced.

getBuiltin :: (HasBuiltins m, MonadTCError m) => BuiltinId -> m Term Source #

getBuiltin' :: HasBuiltins m => BuiltinId -> m (Maybe Term) Source #

Returns Nothing if built-in is not bound or bound to a Prim.

getBuiltinName' :: HasBuiltins m => BuiltinId -> m (Maybe QName) Source #

getBuiltinName_ :: (HasBuiltins m, MonadTCError m) => BuiltinId -> m QName Source #

getBuiltinRewriteRelations :: (HasBuiltins m, MonadTCError m) => m (Set QName) Source #

Get the currently registered rewrite relation symbols.

getBuiltinRewriteRelations' :: HasBuiltins m => m (Maybe (Set QName)) Source #

Get the currently registered rewrite relation symbols, if any.

getName' :: (HasBuiltins m, IsBuiltin a) => a -> m (Maybe QName) Source #

getNameOfConstrained :: HasBuiltins m => PrimitiveId -> m (Maybe QName) Source #

getPrimName :: Term -> QName Source #

getPrimitive :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => PrimitiveId -> m PrimFun Source #

getPrimitive' :: HasBuiltins m => PrimitiveId -> m (Maybe PrimFun) Source #

Returns Nothing if primitive is not bound or bound to a Builtin.

getPrimitiveName' :: HasBuiltins m => PrimitiveId -> m (Maybe QName) Source #

getPrimitiveTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => PrimitiveId -> m Term Source #

getPrimitiveTerm' :: HasBuiltins m => PrimitiveId -> m (Maybe Term) Source #

getTerm :: (HasBuiltins m, IsBuiltin a) => String -> a -> m Term Source #

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) => a -> m (Maybe Term) Source #

infallibleSortKit :: HasBuiltins m => m SortKit Source #

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.

intervalSort :: Sort Source #

intervalUnview :: HasBuiltins m => IntervalView -> m Term Source #

intervalUnview' :: HasBuiltins m => m (IntervalView -> Term) Source #

intervalView :: HasBuiltins m => Term -> m IntervalView Source #

intervalView' :: HasBuiltins m => m (Term -> IntervalView) Source #

isPrimitive :: HasBuiltins m => PrimitiveId -> QName -> m Bool Source #

litType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => Literal -> m Type Source #

mkSortKit :: QName -> QName -> QName -> QName -> QName -> QName -> SortKit Source #

pathUnview :: PathView -> Type Source #

Revert the PathView.

Postcondition: type is reduced.

pathView :: HasBuiltins m => Type -> m PathView Source #

Check whether the type is actually an path (lhs ≡ rhs) and extract lhs, rhs, and their type.

Precondition: type is reduced.

pathView' :: HasBuiltins m => m (Type -> PathView) Source #

primAbs :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAbsAbs :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaBlocker :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaBlockerAll :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaBlockerAny :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaBlockerMeta :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaClause :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaClauseAbsurd :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaClauseClause :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaDefinition :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaDefinitionDataConstructor :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaDefinitionDataDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaDefinitionFunDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaDefinitionPostulate :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaDefinitionPrimitive :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaDefinitionRecordDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaErrorPart :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaErrorPartName :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaErrorPartPatt :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaErrorPartString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaErrorPartTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaLitChar :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaLitFloat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaLitMeta :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaLitNat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaLitQName :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaLitString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaLitWord64 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaLiteral :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaMeta :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaPatAbsurd :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaPatCon :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaPatDot :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaPatLit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaPatProj :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaPatVar :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaPattern :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaSort :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaSortInf :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaSortLit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaSortProp :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaSortPropLit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaSortSet :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaSortUnsupported :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCM :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMAskExpandLast :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMAskNormalisation :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMAskReconstructed :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMAskReduceDefs :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMBind :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMBlock :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMCatchError :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMCheckFromString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMCheckType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMCommit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMDebugPrint :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMDeclareData :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMDeclareDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMDeclarePostulate :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMDefineData :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMDefineFun :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMExec :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMExtendContext :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMFormatErrorParts :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMFreshName :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMGetContext :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMGetDefinition :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMGetInstances :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMGetType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMInContext :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMInferType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMIsMacro :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMNoConstraints :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMNormalise :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMPragmaCompile :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMPragmaForeign :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMQuoteOmegaTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMQuoteTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMReduce :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMReturn :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMRunSpeculative :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMSolveInstances :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMTypeError :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMUnify :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMUnquoteTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMWithExpandLast :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMWithNormalisation :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMWithReconstructed :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMWithReduceDefs :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMWorkOnTypes :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTermCon :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTermDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTermExtLam :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTermLam :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTermLit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTermMeta :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTermPi :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTermSort :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTermUnsupported :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTermVar :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primArg :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primArgArg :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primArgArgInfo :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primArgInfo :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAssoc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAssocLeft :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAssocNon :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAssocRight :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primBool :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primChar :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primCons :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primEquality :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primEqualityName :: TCM QName Source #

Get the name of the equality type.

primEquiv :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primEquivFun :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primEquivProof :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primFaceForall :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primFalse :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primFixity :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primFixityFixity :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primFlat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primFloat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primFromNat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primFromNeg :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primFromString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primGlue :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primHComp :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primHidden :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primHiding :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primIMax :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primIMin :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primINeg :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primIO :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primIOne :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primIZero :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primInf :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primInstance :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primInteger :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primIntegerNegSuc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primIntegerPos :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primInterval :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primIntervalUniv :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primIrrelevant :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primIsOne :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primIsOne1 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primIsOne2 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primIsOneEmpty :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primItIsOne :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primJust :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primLevel :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primLevelMax :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primLevelSuc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primLevelUniv :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primLevelZero :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primList :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primLockUniv :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primMaybe :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primModality :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primModalityConstructor :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primNat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primNatDivSucAux :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primNatEquality :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primNatLess :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primNatMinus :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primNatModSucAux :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primNatPlus :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primNatTimes :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primNil :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primNothing :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primPartial :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primPartialP :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primPath :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primPathP :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primPrecRelated :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primPrecUnrelated :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primPrecedence :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primProp :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primPropOmega :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primQName :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primQuantity :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primQuantity0 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primQuantityω :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primRefl :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primRelevance :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primRelevant :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primSSetOmega :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primSet :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primSetOmega :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primSharp :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primSigma :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primSize :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primSizeInf :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primSizeLt :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primSizeMax :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primSizeSuc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primSizeUniv :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primStrictSet :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primSub :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primSubIn :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primSubOut :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primSuc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primTrans :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primTranspProof :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primTrue :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primUnit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primUnitUnit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primVisible :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primWord64 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primZero :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

prim_glue :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

prim_glueU :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

prim_unglue :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

prim_unglueU :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

runBuiltinAccess :: TCState -> BuiltinAccess a -> a Source #

Run a BuiltinAccess monad.

setBuiltinThings :: BuiltinThings -> TCM () Source #

sortKit :: (HasBuiltins m, MonadTCError m, HasOptions m) => m SortKit Source #

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.

newtype BuiltinAccess a Source #

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.

Constructors

BuiltinAccess 

Fields

Instances

Instances details
HasBuiltins BuiltinAccess Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: SomeBuiltin -> BuiltinAccess (Maybe (Builtin PrimFun)) Source #

Applicative BuiltinAccess Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

pure :: a -> BuiltinAccess a #

(<*>) :: BuiltinAccess (a -> b) -> BuiltinAccess a -> BuiltinAccess b #

liftA2 :: (a -> b -> c) -> BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess c #

(*>) :: BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess b #

(<*) :: BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess a #

Functor BuiltinAccess Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

fmap :: (a -> b) -> BuiltinAccess a -> BuiltinAccess b #

(<$) :: a -> BuiltinAccess b -> BuiltinAccess a #

Monad BuiltinAccess Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

(>>=) :: BuiltinAccess a -> (a -> BuiltinAccess b) -> BuiltinAccess b #

(>>) :: BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess b #

return :: a -> BuiltinAccess a #

MonadFail BuiltinAccess Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

fail :: String -> BuiltinAccess a #

data CoinductionKit Source #

The coinductive primitives.

Constructors

CoinductionKit 

Fields

class EqualityUnview a where Source #

Revert the EqualityView.

Postcondition: type is reduced.

Methods

equalityUnview :: a -> Type Source #

Instances

Instances details
EqualityUnview EqualityTypeData Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

equalityUnview :: EqualityTypeData -> Type Source #

EqualityUnview EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

equalityUnview :: EqualityView -> Type Source #

class (Functor m, Applicative m, Monad m) => HasBuiltins (m :: Type -> Type) where Source #

Minimal complete definition

Nothing

Methods

getBuiltinThing :: SomeBuiltin -> m (Maybe (Builtin PrimFun)) Source #

default getBuiltinThing :: forall (t :: (Type -> Type) -> Type -> Type) (n :: Type -> Type). (MonadTrans t, HasBuiltins n, t n ~ m) => SomeBuiltin -> m (Maybe (Builtin PrimFun)) Source #

Instances

Instances details
HasBuiltins TerM Source # 
Instance details

Defined in Agda.Termination.Monad

Methods

getBuiltinThing :: SomeBuiltin -> TerM (Maybe (Builtin PrimFun)) Source #

HasBuiltins ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Reduce.Monad

Methods

getBuiltinThing :: SomeBuiltin -> ReduceM (Maybe (Builtin PrimFun)) Source #

HasBuiltins BuiltinAccess Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: SomeBuiltin -> BuiltinAccess (Maybe (Builtin PrimFun)) Source #

HasBuiltins NLM Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

getBuiltinThing :: SomeBuiltin -> NLM (Maybe (Builtin PrimFun)) Source #

HasBuiltins m => HasBuiltins (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

getBuiltinThing :: SomeBuiltin -> PureConversionT m (Maybe (Builtin PrimFun)) Source #

HasBuiltins m => HasBuiltins (BlockT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: SomeBuiltin -> BlockT m (Maybe (Builtin PrimFun)) Source #

MonadIO m => HasBuiltins (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: SomeBuiltin -> TCMT m (Maybe (Builtin PrimFun)) Source #

HasBuiltins m => HasBuiltins (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

Methods

getBuiltinThing :: SomeBuiltin -> NamesT m (Maybe (Builtin PrimFun)) Source #

HasBuiltins m => HasBuiltins (ListT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: SomeBuiltin -> ListT m (Maybe (Builtin PrimFun)) Source #

HasBuiltins m => HasBuiltins (ChangeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: SomeBuiltin -> ChangeT m (Maybe (Builtin PrimFun)) Source #

HasBuiltins m => HasBuiltins (MaybeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: SomeBuiltin -> MaybeT m (Maybe (Builtin PrimFun)) Source #

HasBuiltins m => HasBuiltins (ExceptT e m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: SomeBuiltin -> ExceptT e m (Maybe (Builtin PrimFun)) Source #

HasBuiltins m => HasBuiltins (IdentityT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: SomeBuiltin -> IdentityT m (Maybe (Builtin PrimFun)) Source #

HasBuiltins m => HasBuiltins (ReaderT e m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: SomeBuiltin -> ReaderT e m (Maybe (Builtin PrimFun)) Source #

HasBuiltins m => HasBuiltins (StateT s m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: SomeBuiltin -> StateT s m (Maybe (Builtin PrimFun)) Source #

(HasBuiltins m, Monoid w) => HasBuiltins (WriterT w m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: SomeBuiltin -> WriterT w m (Maybe (Builtin PrimFun)) Source #

data SortKit Source #

Sort primitives.

Constructors

SortKit 

Fields

module Agda.Syntax.Builtin