Home
last modified time | relevance | path

Searched refs:exportedNamesInScope (Results 1 – 3 of 3) sorted by relevance

/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/Scope/
H A DBase.hs729 exportedNamesInScope :: InScope a => Scope -> ThingsInScope a
730 exportedNamesInScope = namesInScope [PublicNS, ImportedNS] function
1002 exportedNamesInScope $ mergeScopes $ Map.elems $ publicModules scope
1046 [ qual c (build ms' exportedNamesInScope $ moduleScope a)
1060 build ms' exportedNamesInScope $ moduleScope m
1080 [ qual c (build exportedNamesInScope $ moduleScope a)
1091 build exportedNamesInScope $ moduleScope m
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Rules/
H A DTerm.hs33 , exportedNamesInScope)
932 names = exportedNamesInScope modScope
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Interaction/
H A DBasicOps.hs1263 modules = exportedNamesInScope modScope
1265 names = exportedNamesInScope modScope