Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




Stuff for sized types that does not require modules Agda.TypeChecking.Reduce or Agda.TypeChecking.Constraints (which import Agda.TypeChecking.Monad).


Testing for type Size

data BoundedSize Source

Result of querying whether size variable i is bounded by another size.


BoundedLt Term

yes i : Size< t


isSizeType :: Type -> TCM (Maybe BoundedSize) Source

Check if a type is the primSize type. The argument should be reduced.

haveSizedTypes :: TCM Bool Source

Test whether OPTIONS --sized-types and whether the size built-ins are defined.

builtinSizeHook :: String -> QName -> Type -> TCM () Source

Add polarity info to a SIZE builtin.


sizeSort :: Sort Source

The sort of built-in types SIZE and SIZELT.

sizeUniv :: Type Source

The type of built-in types SIZE and SIZELT.

sizeType_ :: QName -> Type Source

The built-in type SIZE with user-given name.

sizeType :: TCM Type Source

The built-in type SIZE.

sizeSucName :: TCM (Maybe QName) Source

The name of SIZESUC.

sizeMax :: [Term] -> TCM Term Source

Transform list of terms into a term build from binary maximum.

Viewing and unviewing sizes

data SizeView Source

A useful view on sizes.

sizeViewComparable :: DeepSizeView -> DeepSizeView -> SizeViewComparable () Source

sizeViewComparable v w checks whether v >= w (then Left) or v <= w (then Right). If uncomparable, it returns NotComparable.

sizeViewPred :: Nat -> DeepSizeView -> DeepSizeView Source

sizeViewPred k v decrements v by k (must be possible!).

sizeViewOffset :: DeepSizeView -> Maybe Offset Source

sizeViewOffset v returns the number of successors or Nothing when infty.

removeSucs :: (DeepSizeView, DeepSizeView) -> (DeepSizeView, DeepSizeView) Source

Remove successors common to both sides.

unSizeView :: SizeView -> TCM Term Source

Turn a size view into a term.

View on sizes where maximum is pulled to the top

maxViewCons :: DeepSizeView -> SizeMaxView -> SizeMaxView Source

maxViewCons v ws = max v ws. It only adds v to ws if it is not subsumed by an element of ws.

sizeViewComparableWithMax :: DeepSizeView -> SizeMaxView -> SizeViewComparable SizeMaxView Source

sizeViewComparableWithMax v ws tries to find w in ws that compares with v and singles this out. Precondition: v /= DSizeInv.