Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.SizedTypes.Pretty

Synopsis

Documentation

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

Turn a size expression into a term.

Orphan instances

PrettyTCM HypSizeConstraint Source # 
Instance details

PrettyTCM SizeConstraint Source #

Assumes we are in the right context.

Instance details

PrettyTCM SizeMeta Source # 
Instance details