Home
last modified time | relevance | path

Searched refs:anameName (Results 1 – 14 of 14) sorted by relevance

/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Interaction/
H A DSearchAbout.hs41 let userIdentifiers = fmap (fmap anameName . anames) rnms
56 t <- normalForm norm =<< typeOfConst (anameName n)
H A DEmacsTop.hs362 TCP.<+> TCP.text (prettyShow $ anameName a)
365 TCP.nest 2 (pWhy (nameBindingSite $ qnameName $ anameName a) (anameLineage a))
H A DBasicOps.hs1268 d <- getConstInfo $ anameName n
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/Scope/
H A DMonad.hs339 throwError $ A.qualify_ y :| map anameName ys'
350 possibleBaseNames = filter (canHaveSuffix . anameName . fst) $ possibleNames xbase
367 Just ds -> throwError $ fmap (anameName . fst) $ caseMaybe suffixedNames id ((<>) . snd) ds
372 Just (suffix , sds) -> throwError $ fmap (anameName . fst) sds
381 Just ns -> \ f -> filter $ (`Set.member` ns) . A.qnameName . anameName . f
385 updateConcreteName d@(AbsName { anameName = A.QName qm qn }) x =
386 d { anameName = A.QName (setRange (getRange x) qm) (qn { nameConcrete = x }) }
459 notation = namesToNotation x . qnameName . anameName
498 DefinedName _ d _ -> clash $ anameName d
513 then success else clash $ anameName (List1.head ds)
[all …]
H A DBase.hs457 { anameName :: A.QName function
483 (==) = (==) `on` anameName
486 compare = compare `on` anameName
493 lensAnameName f am = f (anameName am) <&> \ m -> am { anameName = m }
710 allANames = Set.fromList . map anameName . concat . Map.elems
792 (Set.insert $ anameName y) -- y is in scope now
1313 (q, k) <- (anameName &&& anameKind) <$> ms
1349 setBindingSite r x = x { anameName = setBindingSite r $ anameName x }
1360 pretty = pretty . anameName
1421 getRange = getRange . anameName
[all …]
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/Translation/
H A DConcreteToAbstract.hs576 raiseWarningsOnUsage $ anameName d
604 let xs = fmap anameName ds
679 DefinedName _ d NoSuffix -> return $ anameName d
1824 let x' = anameName ax
1865 let x' = anameName ax
2178 livesInCurrentModule = livesInCurrentModule . anameName
2374 rebindName acc kind x $ anameName y
2434 ys <- fmap anameName <$> toAbstractExistingName x
2756 FieldName ds -> return $ fmap anameName ds
2842 c = AmbQ (fmap anameName ds)
[all …]
H A DAbstractToConcrete.hs673 toConcrete = toConcrete . anameName
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/
H A DDeadCode.hs28 public <- Set.mapMonotonic anameName . publicNames <$> getScope
H A DPretty.hs336 prettyTCM = prettyTCM . anameName
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Interaction/Highlighting/
H A DFromAbstract.hs439 DefinedName _acc x _suffix -> hilite $ anameName x
440 FieldName xs -> hiliteProjection $ A.AmbQ $ fmap anameName xs
441 ConstructorName i xs -> hiliteAmbiguousQName k $ A.AmbQ $ fmap anameName xs
443 PatternSynResName xs -> hilitePatternSynonym $ A.AmbQ $ fmap anameName xs
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Auto/
H A DAuto.hs434 qnames = map (\(x, y) -> (x, Scope.anameName $ head y)) $ Map.toList names
469 qnames = map (Scope.anameName . head) $ Map.elems names
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/
H A DAbstract.hs941 x = anameName d
954 FieldName xs -> Proj ProjSystem . AmbQ . fmap anameName $ xs
955 ConstructorName _ xs -> Con . AmbQ . fmap anameName $ xs
956 PatternSynResName xs -> PatternSyn . AmbQ . fmap anameName $ xs
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Rules/
H A DBuiltin.hs628 DefinedName _ d NoSuffix -> return $ anameName d
876 unlessM (allM xs $ ((0 ==) . size) <.> lookupSection . qnameModule . anameName) $
909 bind x = bindBuiltinName b (Def (anameName x) [])
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/Concrete/
H A DOperators.hs91 [ mergeNotations $ map (namesToNotation x . A.qnameName . anameName) ds