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