Ensure that option --sized-types is on, for the given reason.
ModuleAgda-2.8.0.2Haskell2010
Agda.TypeChecking.Monad.SizedTypes
Stuff for sized types that does not require modules Agda.TypeChecking.Reduce or Agda.TypeChecking.Constraints (which import Agda.TypeChecking.Monad).
Contents
Synopsis
- value requireOptionSizedTypes
- value getBuiltinSize
- value haveSizeLt
- value builtinSizeHook
- data BoundedSize
- class IsSizeType
- value isSizeTypeTest
- value isSizeNameTest
- value isSizeNameTestRaw
- value sizeSort
- value sizeUniv
- value sizeType_
- value sizeType
- value sizeSucName
- value sizeSuc
- value sizeSuc_
- value sizeMax
- data SizeView
- value sizeView
- data ProjectedVar
- value viewProjectedVar
- value unviewProjectedVar
- type Offset
- data DeepSizeView
- data SizeViewComparable
- value sizeViewComparable
- value sizeViewSuc_
- value sizeViewPred
- value sizeViewOffset
- value removeSucs
- value unSizeView
- value unDeepSizeView
- type SizeMaxView
- type SizeMaxView'
- value maxViewMax
- value maxViewCons
- value sizeViewComparableWithMax
- value maxViewSuc_
- value unMaxView
- PackageAgda-2.8.0.2
- Exports39
- LanguageHaskell2010
- LicenceMIT
- SourceSizedTypes.hs
Builtins
Test whether the SIZELT builtin is defined.
Add polarity info to a SIZE builtin.
Testing for type Size
Result of querying whether size variable i is bounded by another
size.
Instances2Eq, Show
Eq BoundedSizeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.SizedTypesShow BoundedSizeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.SizedTypes
Check if a type is the primSize type. The argument should be reduced.
Methods
isSizeType :: (HasOptions m, HasBuiltins m) => a -> m (Maybe BoundedSize)
Instances5IsSizeType
IsSizeType TermDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.SizedTypesIsSizeType CompareAsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.SizedTypesIsSizeType a => IsSizeType (Dom a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.SizedTypesIsSizeType a => IsSizeType (Type' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.SizedTypesIsSizeType a => IsSizeType (b, a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.SizedTypes
Constructors
The sort of built-in types SIZE and SIZELT.
The type of built-in types SIZE and SIZELT.
The built-in type SIZE with user-given name.
The built-in type SIZE.
The name of SIZESUC.
Transform list of terms into a term build from binary maximum.
Viewing and unviewing sizes
Expects argument to be reduced.
A de Bruijn index under some projections.
Constructors
ProjectedVarpvIndex :: IntprProjs :: [(ProjOrigin, QName)]
Instances2Eq, Show
Eq ProjectedVarDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.SizedTypesIgnore ProjOrigin in equality test.
Show ProjectedVarDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.SizedTypes
A deep view on sizes.
Instances2Show, Pretty
Show DeepSizeViewDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.SizedTypesPretty DeepSizeViewDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.SizedTypes
Constructors
Instances1Functor
Functor SizeViewComparableDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.SizedTypes
sizeViewComparable v w checks whether v >= w (then Left)
or v <= w (then Right). If uncomparable, it returns NotComparable.
sizeViewPred k v decrements v by k (must be possible!).
sizeViewOffset v returns the number of successors or Nothing when infty.
Remove successors common to both sides.
Turn a size view into a term.
View on sizes where maximum is pulled to the top
maxViewCons v ws = max v ws. It only adds v to ws if it is not
subsumed by an element of ws.
sizeViewComparableWithMax v ws tries to find w in ws that compares with v
and singles this out.
Precondition: v /= DSizeInv.