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

Agda.TypeChecking.Level

Synopsis

Documentation

newtype LevelView Source

Constructors

Max [PlusView] 

Instances

data PlusView Source

Constructors

ClosedLevel Integer 
Plus Integer LevelAtom 

Instances

data LevelAtom Source

Constructors

MetaLevel MetaId Args 
BlockedLevel Term 
NeutralLevel Term 

Instances

data LevelKit Source

Constructors

LevelKit 

Fields

levelType :: Term
 
levelSuc :: Term -> Term
 
levelMax :: Term -> Term -> Term
 
levelZero :: Term
 
typeName :: QName
 
sucName :: QName
 
maxName :: QName
 
zeroName :: QName
 

levelSucFunction :: MonadTCM tcm => tcm (Term -> Term)Source

builtinLevelKit :: MonadTCM tcm => tcm (Maybe LevelKit)Source

requireLevels :: TCM LevelKitSource

Raises an error if no level kit is available.

unLevelAtom :: LevelAtom -> TermSource

unLevelView :: MonadTCM tcm => LevelView -> tcm TermSource

maybePrimCon :: MonadTCM tcm => TCM Term -> tcm (Maybe QName)Source

maybePrimDef :: MonadTCM tcm => TCM Term -> tcm (Maybe QName)Source

levelView :: MonadTCM tcm => Term -> tcm LevelViewSource