Agda-2.2.10: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
Agda.TypeChecking.UniversePolymorphism
Documentation
mlevel
::
MonadTCM
tcm => tcm (
Maybe
Term
)
Source
compareLevel
::
MonadTCM
tcm =>
Comparison
->
Term
->
Term
-> tcm
Constraints
Source
warshallConstraint
::
Constraint
->
TCM
[
Constraint
]
Source
solveLevelConstraints
::
TCM
()
Source
Produced by
Haddock
version 2.6.1