Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Monad.Builtin

Synopsis

- class (Functor m, Applicative m, MonadFail m) => HasBuiltins m where
  - getBuiltinThing :: String -> m (Maybe (Builtin PrimFun))
- data SortKit = SortKit {
  - nameOfSet :: QName
  - nameOfProp :: QName
  - nameOfSSet :: QName
  - nameOfSetOmega :: IsFibrant -> QName
  }
- data CoinductionKit = CoinductionKit {
  - nameOfInf :: QName
  - nameOfSharp :: QName
  - nameOfFlat :: QName
  }
- litType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => Literal -> m Type
- setBuiltinThings :: BuiltinThings PrimFun -> TCM ()
- bindBuiltinName :: String -> Term -> TCM ()
- bindPrimitive :: String -> PrimFun -> TCM ()
- getBuiltin :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => String -> m Term
- getBuiltin' :: HasBuiltins m => String -> m (Maybe Term)
- getPrimitive' :: HasBuiltins m => String -> m (Maybe PrimFun)
- getPrimitive :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => String -> m PrimFun
- getPrimitiveTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => String -> m Term
- getPrimitiveTerm' :: HasBuiltins m => String -> m (Maybe Term)
- getTerm' :: HasBuiltins m => String -> m (Maybe Term)
- getName' :: HasBuiltins m => String -> m (Maybe QName)
- getTerm :: HasBuiltins m => String -> String -> m Term
- constructorForm :: HasBuiltins m => Term -> m Term
- constructorForm' :: Applicative m => m Term -> m Term -> Term -> m Term
- primInteger :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primIntegerPos :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primIntegerNegSuc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primFloat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primChar :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primBool :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primSigma :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primUnit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primUnitUnit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primTrue :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primFalse :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primList :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primNil :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primCons :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primMaybe :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primNothing :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primJust :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primIO :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primId :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primConId :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primIdElim :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primPath :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primPathP :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primInterval :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primIZero :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primIOne :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primIMin :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primIMax :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primINeg :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primPartial :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primPartialP :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primIsOne :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primItIsOne :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primTrans :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primHComp :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primEquiv :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primEquivFun :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primEquivProof :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primTranspProof :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- prim_glueU :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- prim_unglueU :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primGlue :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- prim_glue :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- prim_unglue :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primFaceForall :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primIsOne1 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primIsOne2 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primIsOneEmpty :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primSub :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primSubIn :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primSubOut :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primNat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primSuc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primZero :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primNatPlus :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primNatMinus :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primNatTimes :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primNatDivSucAux :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primNatModSucAux :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primNatEquality :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primNatLess :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primWord64 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primSizeUniv :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primSize :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primSizeLt :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primSizeSuc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primSizeInf :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primSizeMax :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primInf :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primSharp :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primFlat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primEquality :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primRefl :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primRewrite :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primLevel :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primLevelZero :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primLevelSuc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primLevelMax :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primSet :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primProp :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primSetOmega :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primLockUniv :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primSSetOmega :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primStrictSet :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primFromNat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primFromNeg :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primFromString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primQName :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primArg :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primArgArg :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAbs :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAbsAbs :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaSort :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primHiding :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primHidden :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primInstance :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primVisible :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primRelevance :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primRelevant :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primIrrelevant :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primQuantity :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primQuantity0 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primQuantityω :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primModality :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primModalityConstructor :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAssoc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAssocLeft :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAssocRight :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAssocNon :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primPrecedence :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primPrecRelated :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primPrecUnrelated :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primFixity :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primFixityFixity :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primArgInfo :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primArgArgInfo :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaSortSet :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaSortLit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaSortProp :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaSortPropLit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaSortInf :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaSortUnsupported :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTermVar :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTermLam :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTermExtLam :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTermDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTermCon :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTermPi :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTermSort :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTermLit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTermUnsupported :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTermMeta :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaErrorPart :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaErrorPartString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaErrorPartTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaErrorPartName :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaLiteral :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaLitNat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaLitWord64 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaLitFloat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaLitChar :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaLitString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaLitQName :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaLitMeta :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaPattern :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaPatCon :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaPatVar :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaPatDot :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaPatLit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaPatProj :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaPatAbsurd :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaClause :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaClauseClause :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaClauseAbsurd :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaDefinitionFunDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaDefinitionDataDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaDefinitionRecordDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaDefinitionDataConstructor :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaDefinitionPostulate :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaDefinitionPrimitive :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaDefinition :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaMeta :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCM :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMReturn :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMBind :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMUnify :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMTypeError :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMInferType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMCheckType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMNormalise :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMReduce :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMCatchError :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMGetContext :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMExtendContext :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMInContext :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMFreshName :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMDeclareDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMDeclarePostulate :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMDefineFun :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMGetType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMGetDefinition :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMQuoteTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMQuoteOmegaTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMUnquoteTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMBlockOnMeta :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMCommit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMIsMacro :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMWithNormalisation :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMWithReconsParams :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMDebugPrint :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMOnlyReduceDefs :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMDontReduceDefs :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMNoConstraints :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMRunSpeculative :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- primAgdaTCMExec :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
- coinductionKit' :: TCM CoinductionKit
- coinductionKit :: TCM (Maybe CoinductionKit)
- sortKit :: HasBuiltins m => m SortKit
- getPrimName :: Term -> QName
- getBuiltinName' :: HasBuiltins m => String -> m (Maybe QName)
- getPrimitiveName' :: HasBuiltins m => String -> m (Maybe QName)
- isPrimitive :: HasBuiltins m => String -> QName -> m Bool
- intervalView' :: HasBuiltins m => m (Term -> IntervalView)
- intervalView :: HasBuiltins m => Term -> m IntervalView
- intervalUnview :: HasBuiltins m => IntervalView -> m Term
- intervalUnview' :: HasBuiltins m => m (IntervalView -> Term)
- pathView :: HasBuiltins m => Type -> m PathView
- pathView' :: HasBuiltins m => m (Type -> PathView)
- idViewAsPath :: HasBuiltins m => Type -> m PathView
- boldPathView :: Type -> PathView
- pathUnview :: PathView -> Type
- primEqualityName :: TCM QName
- equalityView :: Type -> TCM EqualityView
- equalityUnview :: EqualityView -> Type
- constrainedPrims :: [String]
- getNameOfConstrained :: HasBuiltins m => String -> m (Maybe QName)
- module Agda.Syntax.Builtin

# Documentation

class (Functor m, Applicative m, MonadFail m) => HasBuiltins m where Source #

Minimal complete definition

Nothing

Methods

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

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

#### Instances

Instances details

HasBuiltins AbsToCon Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods getBuiltinThing :: String -> AbsToCon (Maybe (Builtin PrimFun)) Source #
HasBuiltins TerM Source # |
Instance details Defined in Agda.Termination.Monad Methods getBuiltinThing :: String -> TerM (Maybe (Builtin PrimFun)) Source #
HasBuiltins ReduceM Source # |
Instance details Defined in Agda.TypeChecking.Reduce.Monad Methods getBuiltinThing :: String -> ReduceM (Maybe (Builtin PrimFun)) Source #
HasBuiltins NLM Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods getBuiltinThing :: String -> NLM (Maybe (Builtin PrimFun)) Source #
HasBuiltins m => HasBuiltins (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods getBuiltinThing :: String -> PureConversionT m (Maybe (Builtin PrimFun)) Source #
HasBuiltins m => HasBuiltins (BlockT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Builtin Methods getBuiltinThing :: String -> BlockT m (Maybe (Builtin PrimFun)) Source #
MonadIO m => HasBuiltins (TCMT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Builtin Methods getBuiltinThing :: String -> TCMT m (Maybe (Builtin PrimFun)) Source #
HasBuiltins m => HasBuiltins (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names Methods getBuiltinThing :: String -> NamesT m (Maybe (Builtin PrimFun)) Source #
HasBuiltins m => HasBuiltins (ListT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Builtin Methods getBuiltinThing :: String -> ListT m (Maybe (Builtin PrimFun)) Source #
HasBuiltins m => HasBuiltins (MaybeT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Builtin Methods getBuiltinThing :: String -> MaybeT m (Maybe (Builtin PrimFun)) Source #
HasBuiltins m => HasBuiltins (ExceptT e m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Builtin Methods getBuiltinThing :: String -> ExceptT e m (Maybe (Builtin PrimFun)) Source #
HasBuiltins m => HasBuiltins (IdentityT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Builtin Methods getBuiltinThing :: String -> IdentityT m (Maybe (Builtin PrimFun)) Source #
HasBuiltins m => HasBuiltins (ReaderT e m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Builtin Methods getBuiltinThing :: String -> ReaderT e m (Maybe (Builtin PrimFun)) Source #
HasBuiltins m => HasBuiltins (StateT s m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Builtin Methods getBuiltinThing :: String -> 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 :: String -> WriterT w m (Maybe (Builtin PrimFun)) Source #

data SortKit Source #

Sort primitives.

Constructors

SortKit |

Fields

- nameOfSet :: QName
- nameOfProp :: QName
- nameOfSSet :: QName
- nameOfSetOmega :: IsFibrant -> QName

data CoinductionKit Source #

The coinductive primitives.

Constructors

CoinductionKit |

Fields

- nameOfInf :: QName
- nameOfSharp :: QName
- nameOfFlat :: QName

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

setBuiltinThings :: BuiltinThings PrimFun -> TCM () Source #

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

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

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

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

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

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

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

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

getTerm' :: HasBuiltins m => String -> m (Maybe Term) Source #

getName' :: HasBuiltins m => String -> m (Maybe QName) Source #

getTerm :: HasBuiltins m => String -> String -> 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.

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 #

primInteger :: (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 #

primIntegerNegSuc :: (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 #

primChar :: (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 #

primBool :: (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 #

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 #

primTrue :: (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 #

primList :: (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 #

primCons :: (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 #

primNothing :: (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 #

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

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

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

primIdElim :: (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 #

primInterval :: (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 #

primIOne :: (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 #

primIMax :: (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 #

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 #

primIsOne :: (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 #

primTrans :: (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 #

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 #

primTranspProof :: (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_unglueU :: (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 #

prim_glue :: (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 #

primFaceForall :: (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 #

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 #

primNat :: (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 #

primZero :: (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 #

primNatMinus :: (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 #

primNatDivSucAux :: (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 #

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 #

primWord64 :: (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 #

primSize :: (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 #

primSizeSuc :: (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 #

primSizeMax :: (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 #

primSharp :: (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 #

primEquality :: (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 #

primRewrite :: (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 #

primLevelZero :: (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 #

primLevelMax :: (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 #

primProp :: (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 #

primLockUniv :: (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 #

primStrictSet :: (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 #

primQName :: (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 #

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 #

primAgdaSort :: (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 #

primHidden :: (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 #

primVisible :: (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 #

primIrrelevant :: (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 #

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 #

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 #

primAssocRight :: (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 #

primPrecedence :: (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 #

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 #

primArgInfo :: (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 #

primAgdaSortSet :: (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 #

primAgdaSortInf :: (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 #

primAgdaTerm :: (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 #

primAgdaTermLam :: (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 #

primAgdaTermDef :: (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 #

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 #

primAgdaTermLit :: (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 #

primAgdaTermMeta :: (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 #

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 #

primAgdaErrorPartName :: (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 #

primAgdaLitNat :: (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 #

primAgdaLitFloat :: (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 #

primAgdaLitString :: (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 #

primAgdaLitMeta :: (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 #

primAgdaPatCon :: (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 #

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 #

primAgdaPatAbsurd :: (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 #

primAgdaClauseClause :: (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 #

primAgdaDefinitionFunDef :: (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 #

primAgdaDefinitionRecordDef :: (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 #

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 #

primAgdaDefinition :: (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 #

primAgdaTCM :: (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 #

primAgdaTCMBind :: (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 #

primAgdaTCMTypeError :: (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 #

primAgdaTCMCheckType :: (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 #

primAgdaTCMReduce :: (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 #

primAgdaTCMGetContext :: (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 #

primAgdaTCMInContext :: (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 #

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 #

primAgdaTCMDefineFun :: (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 #

primAgdaTCMGetDefinition :: (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 #

primAgdaTCMQuoteOmegaTerm :: (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 #

primAgdaTCMBlockOnMeta :: (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 #

primAgdaTCMIsMacro :: (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 #

primAgdaTCMWithReconsParams :: (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 #

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

primAgdaTCMDontReduceDefs :: (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 #

primAgdaTCMRunSpeculative :: (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 #

coinductionKit' :: TCM CoinductionKit Source #

Tries to build a `CoinductionKit`.

coinductionKit :: TCM (Maybe CoinductionKit) Source #

sortKit :: HasBuiltins m => m SortKit Source #

getPrimName :: Term -> QName Source #

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

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

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

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

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

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

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

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 #

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

Non dependent Path

boldPathView :: Type -> PathView Source #

pathUnview :: PathView -> Type Source #

Revert the `PathView`.

Postcondition: type is reduced.

primEqualityName :: TCM QName Source #

Get the name of the equality type.

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.

equalityUnview :: EqualityView -> Type Source #

Revert the `EqualityView`.

Postcondition: type is reduced.

constrainedPrims :: [String] Source #

Primitives with typechecking constrants.

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

module Agda.Syntax.Builtin