ModuleAgda-2.8.0.2Haskell2010
Agda.TypeChecking.Level
Synopsis
- data LevelKit
- value levelType
- value levelType'
- value isLevelType
- value builtinLevelKit
- value requireLevels
- value haveLevels
- value unLevel
- value reallyUnLevelView
- value unlevelWithKit
- value unConstV
- value unPlusV
- value levelView
- value levelView'
- value levelPlusView
- value levelLowerBound
- value subLevel
- value levelMaxDiff
- data SingleLevel'
- type SingleLevel
- value unSingleLevel
- value unSingleLevels
- value levelMaxView
- value singleLevelView
- PackageAgda-2.8.0.2
- Exports24
- LanguageHaskell2010
- LicenceMIT
- SourceLevel.hs
Raises an error if no level kit is available.
Checks whether level kit is fully available.
Given a level l, find the maximum constant n such that l = n + l'
Given a level l, find the biggest constant n such that n <= l
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.
Given two levels a and b, try to decompose the first one as
a = a' ⊔ b (for the minimal value of a').
A SingleLevel is a Level that cannot be further decomposed as
a maximum a ⊔ b.
Constructors
Instances8Eq, Functor, Foldable, Traversable, Show, Subst, …
Eq SingleLevelDefined in Agda-2.8.0.2 · Agda.TypeChecking.LevelFunctor SingleLevel'Defined in Agda-2.8.0.2 · Agda.TypeChecking.LevelFoldable SingleLevel'Defined in Agda-2.8.0.2 · Agda.TypeChecking.LevelTraversable SingleLevel'Defined in Agda-2.8.0.2 · Agda.TypeChecking.LevelShow t => Show (SingleLevel' t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.LevelSubst t => Subst (SingleLevel' t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.LevelFree t => Free (SingleLevel' t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Leveltype SubstArg (SingleLevel' t) = SubstArg tDefined in Agda-2.8.0.2 · Agda.TypeChecking.Level
Return the maximum of the given SingleLevels