Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




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.


sizeMax :: [Term] -> TCM TermSource

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 -> DeepSizeViewSource

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

sizeViewOffset :: DeepSizeView -> Maybe OffsetSource

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 TermSource

Turn a size view into a term.

View on sizes where maximum is pulled to the top

maxViewCons :: DeepSizeView -> SizeMaxView -> SizeMaxViewSource

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 SizeMaxViewSource

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