Text.WebIDL.Types.Identifier

Definitions

IsArgumentNameKeyword : String -> Bool

  Checks, whether a given string corresponds to a WebIDL
  argument name keyword.

Totality: total
Visibility: public export

IsFloatKeyword : String -> Bool

  Checks, whether a given string corresponds to one
  of the floating point constants "NaN", "Infinity", or
  "-Infinity".

Totality: total
Visibility: public export

IsKeyword : String -> Bool

  Checks, whether a given string corresponds to any WebIDL keyword.

Totality: total
Visibility: public export

record Keyword : Type

Totality: total
Visibility: public export
Constructor: 

MkKeyword : (value : String) -> (0 _ : Holds IsKeyword value) -> Keyword

Projections:

0 .isValid : ({rec:0} : Keyword) -> Holds IsKeyword (value {rec:0})

.value : Keyword -> String

Hints:

Eq Keyword

Interpolation Keyword

Ord Keyword

Show Keyword

.value : Keyword -> String

Totality: total
Visibility: public export

value : Keyword -> String

Totality: total
Visibility: public export

0 .isValid : ({rec:0} : Keyword) -> Holds IsKeyword (value {rec:0})

Totality: total
Visibility: public export

0 isValid : ({rec:0} : Keyword) -> Holds IsKeyword (value {rec:0})

Totality: total
Visibility: public export

record ArgumentNameKeyword : Type

Totality: total
Visibility: public export
Constructor: 

MkArgumentNameKeyword : (value : String) -> (0 _ : Holds IsArgumentNameKeyword value) -> ArgumentNameKeyword

Projections:

0 .isValid : ({rec:0} : ArgumentNameKeyword) -> Holds IsArgumentNameKeyword (value {rec:0})

.value : ArgumentNameKeyword -> String

Hints:

Eq ArgumentNameKeyword

Interpolation ArgumentNameKeyword

Ord ArgumentNameKeyword

Show ArgumentNameKeyword

.value : ArgumentNameKeyword -> String

Totality: total
Visibility: public export

value : ArgumentNameKeyword -> String

Totality: total
Visibility: public export

0 .isValid : ({rec:0} : ArgumentNameKeyword) -> Holds IsArgumentNameKeyword (value {rec:0})

Totality: total
Visibility: public export

0 isValid : ({rec:0} : ArgumentNameKeyword) -> Holds IsArgumentNameKeyword (value {rec:0})

Totality: total
Visibility: public export

record AttributeNameKeyword : Type

  Wrapper for one of the attribute name keywords

Totality: total
Visibility: public export
Constructor: 

MkAttributeNameKeyword : (value : String) -> (0 _ : Holds IsAttributeNameKeyword value) -> AttributeNameKeyword

Projections:

0 .isValid : ({rec:0} : AttributeNameKeyword) -> Holds IsAttributeNameKeyword (value {rec:0})

.value : AttributeNameKeyword -> String

Hints:

Eq AttributeNameKeyword

Interpolation AttributeNameKeyword

Ord AttributeNameKeyword

Show AttributeNameKeyword

.value : AttributeNameKeyword -> String

Totality: total
Visibility: public export

value : AttributeNameKeyword -> String

Totality: total
Visibility: public export

0 .isValid : ({rec:0} : AttributeNameKeyword) -> Holds IsAttributeNameKeyword (value {rec:0})

Totality: total
Visibility: public export

0 isValid : ({rec:0} : AttributeNameKeyword) -> Holds IsAttributeNameKeyword (value {rec:0})

Totality: total
Visibility: public export

record Identifier : Type

  Identifier

Totality: total
Visibility: public export
Constructor: 

MkIdent : String -> Identifier

Projection: 

.value : Identifier -> String

Hints:

Eq Identifier

FromString Identifier

HasAttributes Identifier

Interpolation Identifier

Ord Identifier

Show Identifier

.value : Identifier -> String

Totality: total
Visibility: public export

value : Identifier -> String

Totality: total
Visibility: public export

0 IdentifierList : Type

  IdentifierList :: identifier Identifiers
  Identifiers :: "," identifier Identifiers | ε

Totality: total
Visibility: public export

IsIdrisKeyword : String -> Bool

  Checks, if a String corresponds to an Idris2 keyword.

Totality: total
Visibility: public export

data IdrisIdent : Type

  Wrapper type making sure that no Idris2 keyword
  is used as a function's name

Totality: total
Visibility: public export
Constructors:

II : (v : String) -> {auto 0 _ : Holds (not . IsIdrisKeyword) v} -> IdrisIdent

  A string that was successfully checked to be not
  an Idris2 keyword. This can be used without further
  adjustments as an Idris2 identifier.

Prim : String -> IdrisIdent

  Primitive function name. This will be prefixed by
  "prim__" during code generation. As such, the resulting
  identifier always valid in idris.

Underscore : String -> IdrisIdent

  Fallback constructor for Idris2 keywords. An underscore
  will be appended to the wrapped string during code generation.

Hints:

Eq IdrisIdent

FromString IdrisIdent

Interpolation IdrisIdent

Show IdrisIdent

fromIdent : Identifier -> IdrisIdent

Totality: total
Visibility: export