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

Agda.TypeChecking.SizedTypes

Synopsis

- compareSizes :: MonadTCM tcm => Comparison -> Term -> Term -> tcm Constraints
- trivial :: MonadTCM tcm => Term -> Term -> tcm Bool
- getSizeConstraints :: MonadTCM tcm => tcm [SizeConstraint]
- getSizeMetas :: MonadTCM tcm => tcm [(MetaId, Int)]
- data SizeExpr
  - = SizeMeta MetaId [CtxId]
  - | Rigid CtxId
- data SizeConstraint = Leq SizeExpr Int SizeExpr
- computeSizeConstraint :: MonadTCM tcm => ConstraintClosure -> tcm (Maybe SizeConstraint)
- sizeExpr :: MonadTCM tcm => Term -> tcm (SizeExpr, Int)
- flexibleVariables :: SizeConstraint -> [(MetaId, [CtxId])]
- haveSizedTypes :: MonadTCM tcm => tcm Bool
- solveSizeConstraints :: MonadTCM tcm => tcm ()

# Documentation

compareSizes :: MonadTCM tcm => Comparison -> Term -> Term -> tcm Constraints

Compare two sizes. Only with --sized-types.

trivial :: MonadTCM tcm => Term -> Term -> tcm Bool

getSizeConstraints :: MonadTCM tcm => tcm [SizeConstraint]

Find the size constraints.

getSizeMetas :: MonadTCM tcm => tcm [(MetaId, Int)]

data SizeExpr

Constructors

SizeMeta MetaId [CtxId] |
Rigid CtxId |

Instances

Show SizeExpr |

data SizeConstraint

Constructors

Leq SizeExpr Int SizeExpr |

Instances

Show SizeConstraint |

computeSizeConstraint :: MonadTCM tcm => ConstraintClosure -> tcm (Maybe SizeConstraint)

sizeExpr :: MonadTCM tcm => Term -> tcm (SizeExpr, Int)

Throws a `patternViolation` if the term isn't a proper size expression.

flexibleVariables :: SizeConstraint -> [(MetaId, [CtxId])]

haveSizedTypes :: MonadTCM tcm => tcm Bool

solveSizeConstraints :: MonadTCM tcm => tcm ()