Agda-2.6.3.20230930: 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.

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

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.

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

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.

Constructors

SingleClosed Integer 
SinglePlus (PlusLevel' t) 

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

Methods

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

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

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

Methods

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

show :: SingleLevel' t -> String

showList :: [SingleLevel' t] -> ShowS

type SubstArg (SingleLevel' t) Source # 
Instance details

Defined in Agda.TypeChecking.Level

unSingleLevels :: [SingleLevel] -> Level Source #

Return the maximum of the given SingleLevels