Agda.TypeChecking.Level

Documentation

data LevelKit

Constructors

LevelKit

Fields

• lvlType :: Term
• lvlSuc :: Term -> Term
• lvlMax :: Term -> Term -> Term
• lvlZero :: Term
• typeName :: QName
• sucName :: QName
• maxName :: QName
• zeroName :: QName

levelType :: (HasBuiltins m, MonadTCError m) => m Type

Get the primLevel as a Type. Aborts if any of the level BUILTINs is undefined.

levelType' :: HasBuiltins m => m Type

Get the primLevel as a Type. Unsafe, crashes if the BUILTIN LEVEL is undefined.

isLevelType :: PureTCM m => Type -> m Bool

builtinLevelKit :: HasBuiltins m => m LevelKit

requireLevels :: (HasBuiltins m, MonadTCError m) => m LevelKit

Raises an error if no level kit is available.

haveLevels :: HasBuiltins m => m Bool

Checks whether level kit is fully available.

unLevel :: HasBuiltins m => Term -> m Term

reallyUnLevelView :: HasBuiltins m => Level -> m Term

unlevelWithKit :: LevelKit -> Level -> Term

unConstV :: Term -> (Term -> Term) -> Integer -> Term

unPlusV :: (Term -> Term) -> PlusLevel -> Term

maybePrimCon :: TCM Term -> TCM (Maybe ConHead)

maybePrimDef :: TCM Term -> TCM (Maybe QName)

levelView :: PureTCM m => Term -> m Level

levelView' :: PureTCM m => Term -> m Level

levelPlusView :: Level -> (Integer, Level)

Given a level l, find the maximum constant n such that l = n + l'

levelLowerBound :: Level -> Integer

Given a level l, find the biggest constant n such that n <= l

subLevel :: Integer -> Level -> Maybe Level

Given a constant n and a level l, find the level l' such that l = n + l' (or Nothing if there is no such level). Operates on levels in canonical form.

levelMaxDiff :: Level -> Level -> Maybe Level

Given two levels a and b, try to decompose the first one as a = a' ⊔ b (for the minimal value of a').

data SingleLevel' t

A SingleLevel is a Level that cannot be further decomposed as a maximum a ⊔ b.

Constructors

SingleClosed Integer

SinglePlus (PlusLevel' t)

Instances

Functor SingleLevel'

Defined in Agda.TypeChecking.Level

Methods

fmap :: (a -> b) -> SingleLevel' a -> SingleLevel' b

(<$) :: a -> SingleLevel' b -> SingleLevel' a

Foldable SingleLevel'

Defined in Agda.TypeChecking.Level

Methods

fold :: Monoid m => SingleLevel' m -> m

foldMap :: Monoid m => (a -> m) -> SingleLevel' a -> m

foldMap' :: Monoid m => (a -> m) -> SingleLevel' a -> m

foldr :: (a -> b -> b) -> b -> SingleLevel' a -> b

foldr' :: (a -> b -> b) -> b -> SingleLevel' a -> b

foldl :: (b -> a -> b) -> b -> SingleLevel' a -> b

foldl' :: (b -> a -> b) -> b -> SingleLevel' a -> b

foldr1 :: (a -> a -> a) -> SingleLevel' a -> a

foldl1 :: (a -> a -> a) -> SingleLevel' a -> a

toList :: SingleLevel' a -> [a]

null :: SingleLevel' a -> Bool

length :: SingleLevel' a -> Int

elem :: Eq a => a -> SingleLevel' a -> Bool

maximum :: Ord a => SingleLevel' a -> a

minimum :: Ord a => SingleLevel' a -> a

sum :: Num a => SingleLevel' a -> a

product :: Num a => SingleLevel' a -> a

Traversable SingleLevel'

Defined in Agda.TypeChecking.Level

Methods

traverse :: Applicative f => (a -> f b) -> SingleLevel' a -> f (SingleLevel' b)

sequenceA :: Applicative f => SingleLevel' (f a) -> f (SingleLevel' a)

mapM :: Monad m => (a -> m b) -> SingleLevel' a -> m (SingleLevel' b)

sequence :: Monad m => SingleLevel' (m a) -> m (SingleLevel' a)

Eq SingleLevel

Defined in Agda.TypeChecking.Level

Methods

(==) :: SingleLevel -> SingleLevel -> Bool

(/=) :: SingleLevel -> SingleLevel -> Bool

Free t => Free (SingleLevel' t)

Defined in Agda.TypeChecking.Level

Methods

freeVars' :: IsVarSet a c => SingleLevel' t -> FreeM a c

Subst t => Subst (SingleLevel' t)

Defined in Agda.TypeChecking.Level

Associated Types

type SubstArg (SingleLevel' t)

Defined in Agda.TypeChecking.Level

type SubstArg (SingleLevel' t) = SubstArg t

Methods

applySubst :: Substitution' (SubstArg (SingleLevel' t)) -> SingleLevel' t -> SingleLevel' t

Show t => Show (SingleLevel' t)

Defined in Agda.TypeChecking.Level

Methods

showsPrec :: Int -> SingleLevel' t -> ShowS

show :: SingleLevel' t -> String

showList :: [SingleLevel' t] -> ShowS

type SubstArg (SingleLevel' t)

Defined in Agda.TypeChecking.Level

type SubstArg (SingleLevel' t) = SubstArg t

type SingleLevel = SingleLevel' Term

unSingleLevel :: SingleLevel' t -> Level' t

unSingleLevels :: [SingleLevel] -> Level

Return the maximum of the given SingleLevels

levelMaxView :: Level' t -> List1 (SingleLevel' t)

singleLevelView :: Level' t -> Maybe (SingleLevel' t)