Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

addClause f (Clause {namedClausePats = ps}) checks that f ps reduces in a way that agrees with IApply reductions.