Agda-2.2.10: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
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
Source
Compare two sizes. Only with --sized-types.
trivial
::
MonadTCM
tcm =>
Term
->
Term
-> tcm
Bool
Source
getSizeConstraints
::
MonadTCM
tcm => tcm [
SizeConstraint
]
Source
Find the size constraints.
getSizeMetas
::
MonadTCM
tcm => tcm [(
MetaId
,
Int
)]
Source
data
SizeExpr
Source
Constructors
SizeMeta
MetaId
[
CtxId
]
Rigid
CtxId
data
SizeConstraint
Source
Constructors
Leq
SizeExpr
Int
SizeExpr
computeSizeConstraint
::
MonadTCM
tcm =>
ConstraintClosure
-> tcm (
Maybe
SizeConstraint
)
Source
sizeExpr
::
MonadTCM
tcm =>
Term
-> tcm (
SizeExpr
,
Int
)
Source
Throws a
patternViolation
if the term isn't a proper size expression.
flexibleVariables
::
SizeConstraint
-> [(
MetaId
, [
CtxId
])]
Source
haveSizedTypes
::
MonadTCM
tcm => tcm
Bool
Source
solveSizeConstraints
::
MonadTCM
tcm => tcm
()
Source
Produced by
Haddock
version 2.6.1