Agda.TypeChecking.Reduce

instantiate

instantiateFull

reduce

reduceB

normalise

simplify

class Instantiate t

Reduction to weak head normal form.

ifBlocked

ifBlockedType

class Reduce t

rewriteAfter

unfoldCorecursionE

unfoldCorecursion

unfoldDefinition

unfoldDefinitionE

unfoldDefinition'

reduceDefCopy

reduceHead

reduceHead'

appDef_

appDefE_

appDef

appDefE

appDef'

appDefE'

Simplification

class Simplify t

simplifyBlocked'

Normalisation

class Normalise t

Full instantiation

class InstantiateFull t