Agda.TypeChecking.Reduce
instantiate
instantiateFull
reduce
reduceB
normalise
simplify
class Instantiate t
ifBlocked
ifBlockedType
class Reduce t
rewriteAfter
unfoldCorecursionE
unfoldCorecursion
unfoldDefinition
unfoldDefinitionE
unfoldDefinition'
reduceDefCopy
reduceHead
reduceHead'
appDef_
appDefE_
appDef
appDefE
appDef'
appDefE'
class Simplify t
simplifyBlocked'
class Normalise t
class InstantiateFull t