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

Safe Haskell | Safe-Infered

Agda.TypeChecking.SizedTypes

Synopsis

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

# Documentation

compareSizes :: Comparison -> Term -> Term -> TCM ()

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

trivial :: Term -> Term -> TCM Bool

getSizeConstraints :: TCM [SizeConstraint]

Find the size constraints.

getSizeMetas :: 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 :: Closure Constraint -> TCM (Maybe SizeConstraint)

sizeExpr :: Term -> TCM (SizeExpr, Int)

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

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

haveSizedTypes :: TCM Bool

solveSizeConstraints :: TCM ()