ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.Monad.Builtin

Synopsis

value bindBuiltinName
value bindBuiltinRewriteRelation
value bindPrimitive
value boldPathView
value coinductionKit
value coinductionKit'
value constrainedPrims
value constructorForm
value constructorForm'
value equalityView
value getBuiltin
value getBuiltin'
value getBuiltinName'
value getBuiltinName_
value getBuiltinRewriteRelations
value getBuiltinRewriteRelations'
value getName'
value getNameOfConstrained
value getPrimName
value getPrimitive
value getPrimitive'
value getPrimitiveName'
value getPrimitiveTerm
value getPrimitiveTerm'
value getTerm
value getTerm'
value infallibleSortKit
value intervalSort
value intervalUnview
value intervalUnview'
value intervalView
value intervalView'
value isPrimitive
value litType
value mkSortKit
value pathUnview
value pathView
value pathView'
value primAbs
value primAbsAbs
value primAgdaBlocker
value primAgdaBlockerAll
value primAgdaBlockerAny
value primAgdaBlockerMeta
value primAgdaClause
value primAgdaClauseAbsurd
value primAgdaClauseClause
value primAgdaDefinition
value primAgdaDefinitionDataConstructor
value primAgdaDefinitionDataDef
value primAgdaDefinitionFunDef
value primAgdaDefinitionPostulate
value primAgdaDefinitionPrimitive
value primAgdaDefinitionRecordDef
value primAgdaErrorPart
value primAgdaErrorPartName
value primAgdaErrorPartPatt
value primAgdaErrorPartString
value primAgdaErrorPartTerm
value primAgdaLitChar
value primAgdaLitFloat
value primAgdaLitMeta
value primAgdaLitNat
value primAgdaLitQName
value primAgdaLitString
value primAgdaLitWord64
value primAgdaLiteral
value primAgdaMeta
value primAgdaPatAbsurd
value primAgdaPatCon
value primAgdaPatDot
value primAgdaPatLit
value primAgdaPatProj
value primAgdaPatVar
value primAgdaPattern
value primAgdaSort
value primAgdaSortInf
value primAgdaSortLit
value primAgdaSortProp
value primAgdaSortPropLit
value primAgdaSortSet
value primAgdaSortUnsupported
value primAgdaTCM
value primAgdaTCMAskExpandLast
value primAgdaTCMAskNormalisation
value primAgdaTCMAskReconstructed
value primAgdaTCMAskReduceDefs
value primAgdaTCMBind
value primAgdaTCMBlock
value primAgdaTCMCatchError
value primAgdaTCMCheckFromString
value primAgdaTCMCheckType
value primAgdaTCMCommit
value primAgdaTCMDebugPrint
value primAgdaTCMDeclareData
value primAgdaTCMDeclareDef
value primAgdaTCMDeclarePostulate
value primAgdaTCMDefineData
value primAgdaTCMDefineFun
value primAgdaTCMExec
value primAgdaTCMExtendContext
value primAgdaTCMFormatErrorParts
value primAgdaTCMFreshName
value primAgdaTCMGetContext
value primAgdaTCMGetDefinition
value primAgdaTCMGetInstances
value primAgdaTCMGetType
value primAgdaTCMInContext
value primAgdaTCMInferType
value primAgdaTCMIsMacro
value primAgdaTCMNoConstraints
value primAgdaTCMNormalise
value primAgdaTCMPragmaCompile
value primAgdaTCMPragmaForeign
value primAgdaTCMQuoteOmegaTerm
value primAgdaTCMQuoteTerm
value primAgdaTCMReduce
value primAgdaTCMReturn
value primAgdaTCMRunSpeculative
value primAgdaTCMSolveInstances
value primAgdaTCMTypeError
value primAgdaTCMUnify
value primAgdaTCMUnquoteTerm
value primAgdaTCMWithExpandLast
value primAgdaTCMWithNormalisation
value primAgdaTCMWithReconstructed
value primAgdaTCMWithReduceDefs
value primAgdaTCMWorkOnTypes
value primAgdaTerm
value primAgdaTermCon
value primAgdaTermDef
value primAgdaTermExtLam
value primAgdaTermLam
value primAgdaTermLit
value primAgdaTermMeta
value primAgdaTermPi
value primAgdaTermSort
value primAgdaTermUnsupported
value primAgdaTermVar
value primArg
value primArgArg
value primArgArgInfo
value primArgInfo
value primAssoc
value primAssocLeft
value primAssocNon
value primAssocRight
value primBool
value primChar
value primCons
value primEquality
value primEqualityName
value primEquiv
value primEquivFun
value primEquivProof
value primFaceForall
value primFalse
value primFixity
value primFixityFixity
value primFlat
value primFloat
value primFromNat
value primFromNeg
value primFromString
value primGlue
value primHComp
value primHidden
value primHiding
value primIMax
value primIMin
value primINeg
value primIO
value primIOne
value primIZero
value primInf
value primInstance
value primInteger
value primIntegerNegSuc
value primIntegerPos
value primInterval
value primIntervalUniv
value primIrrelevant
value primIsOne
value primIsOne1
value primIsOne2
value primIsOneEmpty
value primItIsOne
value primJust
value primLevel
value primLevelMax
value primLevelSuc
value primLevelUniv
value primLevelZero
value primList
value primLockUniv
value primMaybe
value primModality
value primModalityConstructor
value primNat
value primNatDivSucAux
value primNatEquality
value primNatLess
value primNatMinus
value primNatModSucAux
value primNatPlus
value primNatTimes
value primNil
value primNothing
value primPartial
value primPartialP
value primPath
value primPathP
value primPrecRelated
value primPrecUnrelated
value primPrecedence
value primProp
value primPropOmega
value primQName
value primQuantity
value primQuantity0
value primQuantityω
value primRefl
value primRelevance
value primRelevant
value primSSetOmega
value primSet
value primSetOmega
value primSharp
value primSigma
value primSize
value primSizeInf
value primSizeLt
value primSizeMax
value primSizeSuc
value primSizeUniv
value primStrictSet
value primString
value primSub
value primSubIn
value primSubOut
value primSuc
value primTrans
value primTranspProof
value primTrue
value primUnit
value primUnitUnit
value primVisible
value primWord64
value primZero
value prim_glue
value prim_glueU
value prim_unglue
value prim_unglueU
value runBuiltinAccess
value setBuiltinThings
value sortKit
newtype BuiltinAccess
data CoinductionKit
class EqualityUnview
class HasBuiltins
data SortKit

PackageAgda-2.8.0.2
Exports261
LanguageHaskell2010
LicenceMIT
SourceBuiltin.hs

valuebindBuiltinName :: BuiltinId -> Term -> TCM ()

valuebindBuiltinRewriteRelation :: QName -> TCM ()

Source#

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

valuebindPrimitive :: PrimitiveId -> PrimFun -> TCM ()

valueboldPathView :: Type -> PathView

valuecoinductionKit :: TCM (Maybe CoinductionKit)

valuecoinductionKit' :: TCM CoinductionKit

Source#

Tries to build a CoinductionKit.

valueconstrainedPrims :: [PrimitiveId]

Source#

Primitives with typechecking constrants.

valueconstructorForm :: HasBuiltins m => Term -> m Term

Source#

Rewrite a literal to constructor form if possible.

valueconstructorForm' :: Applicative m => m Term -> m Term -> Term -> m Term

valueequalityView

:: Range
Range of the rewrite expression, if any.
-> Type
Identity 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.

valuegetBuiltin :: (HasBuiltins m, MonadTCError m) => BuiltinId -> m Term

valuegetBuiltin' :: HasBuiltins m => BuiltinId -> m (Maybe Term)

Source#

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

valuegetBuiltinName' :: HasBuiltins m => BuiltinId -> m (Maybe QName)

valuegetBuiltinName_ :: (HasBuiltins m, MonadTCError m) => BuiltinId -> m QName

valuegetBuiltinRewriteRelations :: (HasBuiltins m, MonadTCError m) => m (Set QName)

Source#

Get the currently registered rewrite relation symbols.

valuegetBuiltinRewriteRelations' :: HasBuiltins m => m (Maybe (Set QName))

Source#

Get the currently registered rewrite relation symbols, if any.

valuegetName' :: (HasBuiltins m, IsBuiltin a) => a -> m (Maybe QName)

valuegetNameOfConstrained :: HasBuiltins m => PrimitiveId -> m (Maybe QName)

valuegetPrimName :: Term -> QName

valuegetPrimitive

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

valuegetPrimitive' :: HasBuiltins m => PrimitiveId -> m (Maybe PrimFun)

Source#

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

valuegetPrimitiveName' :: HasBuiltins m => PrimitiveId -> m (Maybe QName)

valuegetPrimitiveTerm

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

valuegetPrimitiveTerm' :: HasBuiltins m => PrimitiveId -> m (Maybe Term)

valuegetTerm :: (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.

valuegetTerm' :: (HasBuiltins m, IsBuiltin a) => a -> m (Maybe Term)

valueinfallibleSortKit :: 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.

valueintervalSort :: Sort

valueintervalUnview :: HasBuiltins m => IntervalView -> m Term

valueintervalUnview' :: HasBuiltins m => m (IntervalView -> Term)

valueintervalView :: HasBuiltins m => Term -> m IntervalView

valueintervalView' :: HasBuiltins m => m (Term -> IntervalView)

valueisPrimitive :: HasBuiltins m => PrimitiveId -> QName -> m Bool

valuelitType

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

valuemkSortKit :: QName -> QName -> QName -> QName -> QName -> QName -> SortKit

valuepathUnview :: PathView -> Type

Source#

Revert the PathView.

Postcondition: type is reduced.

valuepathView :: 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.

valuepathView' :: HasBuiltins m => m (Type -> PathView)

valueprimAbs :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAbsAbs :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaBlocker :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaBlockerAll :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaBlockerAny :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaBlockerMeta :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaClause :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaClauseAbsurd :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaClauseClause :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaDefinition :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaDefinitionDataConstructor :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaDefinitionDataDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaDefinitionFunDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaDefinitionPostulate :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaDefinitionPrimitive :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaDefinitionRecordDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaErrorPart :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaErrorPartName :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaErrorPartPatt :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaErrorPartString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaErrorPartTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaLitChar :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaLitFloat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaLitMeta :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaLitNat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaLitQName :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaLitString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaLitWord64 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaLiteral :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaMeta :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaPatAbsurd :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaPatCon :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaPatDot :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaPatLit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaPatProj :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaPatVar :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaPattern :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaSort :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaSortInf :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaSortLit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaSortProp :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaSortPropLit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaSortSet :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaSortUnsupported :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCM :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMAskExpandLast :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMAskNormalisation :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMAskReconstructed :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMAskReduceDefs :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMBind :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMBlock :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMCatchError :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMCheckFromString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMCheckType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMCommit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMDebugPrint :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMDeclareData :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMDeclareDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMDeclarePostulate :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMDefineData :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMDefineFun :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMExec :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMExtendContext :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMFormatErrorParts :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMFreshName :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMGetContext :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMGetDefinition :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMGetInstances :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMGetType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMInContext :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMInferType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMIsMacro :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMNoConstraints :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMNormalise :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMPragmaCompile :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMPragmaForeign :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMQuoteOmegaTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMQuoteTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMReduce :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMReturn :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMRunSpeculative :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMSolveInstances :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMTypeError :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMUnify :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMUnquoteTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMWithExpandLast :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMWithNormalisation :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMWithReconstructed :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMWithReduceDefs :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTCMWorkOnTypes :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTermCon :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTermDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTermExtLam :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTermLam :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTermLit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTermMeta :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTermPi :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTermSort :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTermUnsupported :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAgdaTermVar :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimArg :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimArgArg :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimArgArgInfo :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimArgInfo :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAssoc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAssocLeft :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAssocNon :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimAssocRight :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimBool :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimChar :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimCons :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimEquality :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimEqualityName :: TCM QName

Source#

Get the name of the equality type.

valueprimEquiv :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimEquivFun :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimEquivProof :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimFaceForall :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimFalse :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimFixity :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimFixityFixity :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimFlat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimFloat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimFromNat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimFromNeg :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimFromString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimGlue :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimHComp :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimHidden :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimHiding :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimIMax :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimIMin :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimINeg :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimIO :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimIOne :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimIZero :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimInf :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimInstance :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimInteger :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimIntegerNegSuc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimIntegerPos :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimInterval :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimIntervalUniv :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimIrrelevant :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimIsOne :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimIsOne1 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimIsOne2 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimIsOneEmpty :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimItIsOne :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimJust :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimLevel :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimLevelMax :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimLevelSuc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimLevelUniv :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimLevelZero :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimList :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimLockUniv :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimMaybe :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimModality :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimModalityConstructor :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimNat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimNatDivSucAux :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimNatEquality :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimNatLess :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimNatMinus :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimNatModSucAux :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimNatPlus :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimNatTimes :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimNil :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimNothing :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimPartial :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimPartialP :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimPath :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimPathP :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimPrecRelated :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimPrecUnrelated :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimPrecedence :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimProp :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimPropOmega :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimQName :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimQuantity :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimQuantity0 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimQuantityω :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimRefl :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimRelevance :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimRelevant :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimSSetOmega :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimSet :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimSetOmega :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimSharp :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimSigma :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimSize :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimSizeInf :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimSizeLt :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimSizeMax :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimSizeSuc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimSizeUniv :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimStrictSet :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimSub :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimSubIn :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimSubOut :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimSuc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimTrans :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimTranspProof :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimTrue :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimUnit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimUnitUnit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimVisible :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimWord64 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprimZero :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprim_glue :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprim_glueU :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprim_unglue :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valueprim_unglueU :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

valuerunBuiltinAccess :: TCState -> BuiltinAccess a -> a

Source#

Run a BuiltinAccess monad.

valuesetBuiltinThings :: BuiltinThings -> TCM ()

valuesortKit :: (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.

newtypenewtype 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
- unBuiltinAccess :: TCState -> a

Instances5Monad, Functor, MonadFail, Applicative, HasBuiltins

Monad BuiltinAccessDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Builtin
Functor BuiltinAccessDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Builtin
MonadFail BuiltinAccessDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Builtin
Applicative BuiltinAccessDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Builtin
HasBuiltins BuiltinAccessDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Builtin

datadata CoinductionKit

Source#

The coinductive primitives.

Constructors

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

classclass EqualityUnview a where

Source#

Revert the EqualityView.

Postcondition: type is reduced.

Methods

equalityUnview :: a -> Type

Instances2EqualityUnview

EqualityUnview EqualityTypeDataDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Builtin
EqualityUnview EqualityViewDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Builtin

classclass (Functor m, Applicative m, Monad m) => HasBuiltins (m :: Type -> Type) where

Methods

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

Instances17HasBuiltins, …

HasBuiltins TerMDefined in Agda-2.8.0.2 · Agda.Termination.Monad
HasBuiltins ReduceMDefined in Agda-2.8.0.2 · Agda.TypeChecking.Reduce.Monad · orphan
HasBuiltins BuiltinAccessDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Builtin
HasBuiltins NLMDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.NonLinMatch
HasBuiltins m => HasBuiltins (AbsToConT m)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
HasBuiltins m => HasBuiltins (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.Pure
HasBuiltins m => HasBuiltins (BlockT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Builtin
HasBuiltins m => HasBuiltins (NamesT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Names
HasBuiltins m => HasBuiltins (ListT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Builtin
HasBuiltins m => HasBuiltins (ChangeT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Builtin
HasBuiltins m => HasBuiltins (MaybeT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Builtin
MonadIO m => HasBuiltins (TCMT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Builtin
HasBuiltins m => HasBuiltins (ExceptT e m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Builtin
HasBuiltins m => HasBuiltins (IdentityT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Builtin
HasBuiltins m => HasBuiltins (ReaderT e m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Builtin
HasBuiltins m => HasBuiltins (StateT s m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Builtin
(HasBuiltins m, Monoid w) => HasBuiltins (WriterT w m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Builtin

datadata SortKit

Source#

Sort primitives.

Constructors

SortKit
- nameOfUniv :: UnivSize -> Univ -> QName
- isNameOfUniv :: QName -> Maybe (UnivSize, Univ)

module Agda.Syntax.Builtin