Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.SizedTypes.Pretty

Contents

- Orphan instances

Synopsis

- unSizeExpr :: HasBuiltins m => DBSizeExpr -> m Term

# Documentation

unSizeExpr :: HasBuiltins m => DBSizeExpr -> m Term Source #

Turn a size expression into a term.

# Orphan instances

PrettyTCM HypSizeConstraint Source # |
Instance details Methods prettyTCM :: MonadPretty m => HypSizeConstraint -> m Doc Source #
PrettyTCM SizeConstraint Source # | Assumes we are in the right context.
Instance details Methods prettyTCM :: MonadPretty m => SizeConstraint -> m Doc Source #
PrettyTCM SizeMeta Source # |
Instance details Methods prettyTCM :: MonadPretty m => SizeMeta -> m Doc Source #