Agda.TypeChecking.Irrelevance

Operations on Dom.

hideAndRelParams

inverseApplyRelevance

applyRelevance

Operations on Context.

workOnTypes

doWorkOnTypes

workOnTypes'

applyRelevanceToContext

wakeIrrelevantVars

Tests

prop_galois

tests