Searched refs:emptyScopeInfo (Results 1 – 5 of 5) sorted by relevance
24 import Agda.Syntax.Scope.Base (ScopeInfo, emptyScopeInfo)44 , metaScope = emptyScopeInfo
136 liftTCM $ setScope $ maybe emptyScopeInfo iInsideScope (crInterface <$> checked)
601 empty = emptyScopeInfo618 emptyScopeInfo :: ScopeInfo619 emptyScopeInfo = ScopeInfo function
32 , emptyScopeInfo1445 , A.metaScope = emptyScopeInfo
370 , stPreScope = emptyScopeInfo