Home
last modified time | relevance | path

Searched refs:stringNameParts (Results 1 – 4 of 4) sorted by relevance

/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/Concrete/
H A DName.hs179 stringNameParts :: String -> NameParts
180 stringNameParts "" = singleton $ Id "_" -- NoName function
181 stringNameParts "_" = singleton $ Id "_" -- NoName function
182 stringNameParts s = List1.fromList $ loop s function
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/Abstract/
H A DName.hs189 mkName r i s = makeName i (C.Name noRange InScope (C.stringNameParts s)) r noFixity' False
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Interaction/
H A DMakeCase.hs102 let cname = C.QName $ C.Name r C.InScope $ C.stringNameParts s
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/Translation/
H A DAbstractToConcrete.hs308 return (C.QName $ C.Name noRange C.InScope $ C.stringNameParts s)