Idris2Doc : Lana.Name
Definitions
record Name : Type- Totality: total
Visibility: public export
Constructor: MkName : Maybe String -> String -> Name
Projections:
.nameQualification : Name -> Maybe String .nameUnqualified : Name -> String
.nameQualification : Name -> Maybe String- Visibility: public export
nameQualification : Name -> Maybe String- Visibility: public export
.nameUnqualified : Name -> String- Visibility: public export
nameUnqualified : Name -> String- Visibility: public export
unqualifiedName : String -> Name- Visibility: export
annotateName : Name -> String -> Name- Visibility: export
nameToString : Name -> String- Visibility: export