Agda-2.6.3.20230805: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Level

Synopsis

Documentation

data LevelKit Source #

Constructors

LevelKit 

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

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

levelType' :: HasBuiltins m => m Type Source #

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

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

Raises an error if no level kit is available.

haveLevels :: HasBuiltins m => m Bool Source #

Checks whether level kit is fully available.

levelPlusView :: Level -> (Integer, Level) Source #

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

levelLowerBound :: Level -> Integer Source #

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

subLevel :: Integer -> Level -> Maybe Level Source #

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 Source #

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 Source #

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

Instances

Instances details
Foldable SingleLevel' Source # 
Instance details

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' Source # 
Instance details

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) #

Functor SingleLevel' Source # 
Instance details

Defined in Agda.TypeChecking.Level

Methods

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

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

Eq SingleLevel Source # 
Instance details

Defined in Agda.TypeChecking.Level

Free t => Free (SingleLevel' t) Source # 
Instance details

Defined in Agda.TypeChecking.Level

Methods

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

Subst t => Subst (SingleLevel' t) Source # 
Instance details

Defined in Agda.TypeChecking.Level

Associated Types

type SubstArg (SingleLevel' t) Source #

Show t => Show (SingleLevel' t) Source # 
Instance details

Defined in Agda.TypeChecking.Level

type SubstArg (SingleLevel' t) Source # 
Instance details

Defined in Agda.TypeChecking.Level

unSingleLevels :: [SingleLevel] -> Level Source #

Return the maximum of the given SingleLevels