Agda.TypeChecking.Reduce
class Instantiate t
class Reduce t

Normalisation

class Normalise t

Full instantiation