Agda.TypeChecking.Irrelevance

Operations on Dom.

hideAndRelParams

inverseApplyRelevance

applyRelevance

Operations on Context.

workOnTypes

workOnTypes'

applyRelevanceToContext

wakeIrrelevantVars