| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.SizedTypes.Pretty
Contents
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 # | |
Methods prettyTCM :: MonadPretty m => HypSizeConstraint -> m Doc Source # | |
| PrettyTCM SizeConstraint Source # | Assumes we are in the right context. |
Methods prettyTCM :: MonadPretty m => SizeConstraint -> m Doc Source # | |
| PrettyTCM SizeMeta Source # | |