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).
- 8 types
- 1 class
- 30 values
- PackageAgda-2.8.0.2
- Exports39
- LanguageHaskell2010
- LicenceMIT
- SourceSizedTypes.hs
Builtins
4 declarationsTest whether the SIZELT builtin is defined.
Add polarity info to a SIZE builtin.
Testing for type Size
5 declarationsResult 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
8 declarationsThe 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
15 declarationsExpects 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
7 declarationsmaxViewCons 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.