Agda.TypeChecking.InstanceArguments

initialIFSCandidates

findInScope

findInScope'

insidePi

rigidlyConstrainedMetas

isRigid

areThereNonRigidMetaArguments

filterResetingState

dropSameCandidates

data YesNoMaybe

checkCandidates

isIFSConstraint

applyDroppingParameters