Agda.TypeChecking.Rewriting.NonLinMatch
class PatternFrom a b
type NLM
type NLMState
liftRed
runNLM
traceSDocNLM
matchingBlocked
tellSub
tellEq
type Sub
data PostponedEquation
type PostponedEquations
class Match a b
makeSubstitution
checkPostponedEquations
nonLinMatch
equal
class RaiseNLP a