Idris2Doc : Lana.Name

Lana.Name

(source)

Definitions

recordName : Type
Totality: total
Visibility: public export
Constructor: 
MkName : MaybeString->String->Name

Projections:
.nameQualification : Name->MaybeString
.nameUnqualified : Name->String
.nameQualification : Name->MaybeString
Visibility: public export
nameQualification : Name->MaybeString
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