Idris2Doc : Text.WebIDL.Types.Definition

Text.WebIDL.Types.Definition

(source)
Definitions
record Callback : Type
  CallbackRest ::
      identifier = Type ( ArgumentList ) ;

  Totality: total
  Visibility: public export
  Constructor: 
MkCallback : ExtAttributeList -> Identifier -> IdlType -> ArgumentList -> Callback

  Projections:
  
.args : Callback -> ArgumentList
  
.attributes : Callback -> ExtAttributeList
  
.name : Callback -> Identifier
  
.type : Callback -> IdlType

  Hints:
  
Eq Callback
  
HasAttributes Callback
  
Show Callback
.attributes : Callback -> ExtAttributeList
  Visibility: public export
attributes : Callback -> ExtAttributeList
  Visibility: public export
.name : Callback -> Identifier
  Visibility: public export
name : Callback -> Identifier
  Visibility: public export
.type : Callback -> IdlType
  Visibility: public export
type : Callback -> IdlType
  Visibility: public export
.args : Callback -> ArgumentList
  Visibility: public export
args : Callback -> ArgumentList
  Visibility: public export
record CallbackInterface : Type
  CallbackRestOrInterface ::
      CallbackRest
      interface identifier { CallbackInterfaceMembers } ;

  Totality: total
  Visibility: public export
  Constructor: 
MkCallbackInterface : ExtAttributeList -> Identifier -> CallbackInterfaceMembers -> CallbackInterface

  Projections:
  
.attributes : CallbackInterface -> ExtAttributeList
  
.members : CallbackInterface -> CallbackInterfaceMembers
  
.name : CallbackInterface -> Identifier

  Hints:
  
Eq CallbackInterface
  
HasAttributes CallbackInterface
  
Show CallbackInterface
.attributes : CallbackInterface -> ExtAttributeList
  Visibility: public export
attributes : CallbackInterface -> ExtAttributeList
  Visibility: public export
.name : CallbackInterface -> Identifier
  Visibility: public export
name : CallbackInterface -> Identifier
  Visibility: public export
.members : CallbackInterface -> CallbackInterfaceMembers
  Visibility: public export
members : CallbackInterface -> CallbackInterfaceMembers
  Visibility: public export
record Dictionary : Type
  Dictionary ::
      dictionary identifier Inheritance { DictionaryMembers } ;

  Totality: total
  Visibility: public export
  Constructor: 
MkDictionary : ExtAttributeList -> Identifier -> Inheritance -> DictionaryMembers -> Dictionary

  Projections:
  
.attributes : Dictionary -> ExtAttributeList
  
.inherits : Dictionary -> Inheritance
  
.members : Dictionary -> DictionaryMembers
  
.name : Dictionary -> Identifier

  Hints:
  
Eq Dictionary
  
HasAttributes Dictionary
  
Show Dictionary
.attributes : Dictionary -> ExtAttributeList
  Visibility: public export
attributes : Dictionary -> ExtAttributeList
  Visibility: public export
.name : Dictionary -> Identifier
  Visibility: public export
name : Dictionary -> Identifier
  Visibility: public export
.inherits : Dictionary -> Inheritance
  Visibility: public export
inherits : Dictionary -> Inheritance
  Visibility: public export
.members : Dictionary -> DictionaryMembers
  Visibility: public export
members : Dictionary -> DictionaryMembers
  Visibility: public export
record Enum : Type
  Enum ::
      enum identifier { EnumValueList } ;
  
  EnumValueList ::
      string EnumValueListComma
  
  EnumValueListComma ::
      , EnumValueListString
      ε
  
  EnumValueListString ::
      string EnumValueListComma
      ε

  Totality: total
  Visibility: public export
  Constructor: 
MkEnum : ExtAttributeList -> Identifier -> List1 StringLit -> Enum

  Projections:
  
.attributes : Enum -> ExtAttributeList
  
.name : Enum -> Identifier
  
.values : Enum -> List1 StringLit

  Hints:
  
Eq Enum
  
HasAttributes Enum
  
Show Enum
.attributes : Enum -> ExtAttributeList
  Visibility: public export
attributes : Enum -> ExtAttributeList
  Visibility: public export
.name : Enum -> Identifier
  Visibility: public export
name : Enum -> Identifier
  Visibility: public export
.values : Enum -> List1 StringLit
  Visibility: public export
values : Enum -> List1 StringLit
  Visibility: public export
record Includes : Type
  IncludesStatement ::
      identifier includes identifier ;

  Totality: total
  Visibility: public export
  Constructor: 
MkIncludes : ExtAttributeList -> Identifier -> Identifier -> Includes

  Projections:
  
.attributes : Includes -> ExtAttributeList
  
.includes : Includes -> Identifier
  
.name : Includes -> Identifier

  Hints:
  
Eq Includes
  
HasAttributes Includes
  
Show Includes
.attributes : Includes -> ExtAttributeList
  Visibility: public export
attributes : Includes -> ExtAttributeList
  Visibility: public export
.name : Includes -> Identifier
  Visibility: public export
name : Includes -> Identifier
  Visibility: public export
.includes : Includes -> Identifier
  Visibility: public export
includes : Includes -> Identifier
  Visibility: public export
record Interface : Type
  InterfaceRest ::
      identifier Inheritance { InterfaceMembers } ;

  Totality: total
  Visibility: public export
  Constructor: 
MkInterface : ExtAttributeList -> Identifier -> Inheritance -> InterfaceMembers -> Interface

  Projections:
  
.attributes : Interface -> ExtAttributeList
  
.inherits : Interface -> Inheritance
  
.members : Interface -> InterfaceMembers
  
.name : Interface -> Identifier

  Hints:
  
Eq Interface
  
HasAttributes Interface
  
Show Interface
.attributes : Interface -> ExtAttributeList
  Visibility: public export
attributes : Interface -> ExtAttributeList
  Visibility: public export
.name : Interface -> Identifier
  Visibility: public export
name : Interface -> Identifier
  Visibility: public export
.inherits : Interface -> Inheritance
  Visibility: public export
inherits : Interface -> Inheritance
  Visibility: public export
.members : Interface -> InterfaceMembers
  Visibility: public export
members : Interface -> InterfaceMembers
  Visibility: public export
record Mixin : Type
  MixinRest ::
      mixin identifier { MixinMembers } ;

  Totality: total
  Visibility: public export
  Constructor: 
MkMixin : ExtAttributeList -> Identifier -> MixinMembers -> Mixin

  Projections:
  
.attributes : Mixin -> ExtAttributeList
  
.members : Mixin -> MixinMembers
  
.name : Mixin -> Identifier

  Hints:
  
Eq Mixin
  
HasAttributes Mixin
  
Show Mixin
.attributes : Mixin -> ExtAttributeList
  Visibility: public export
attributes : Mixin -> ExtAttributeList
  Visibility: public export
.name : Mixin -> Identifier
  Visibility: public export
name : Mixin -> Identifier
  Visibility: public export
.members : Mixin -> MixinMembers
  Visibility: public export
members : Mixin -> MixinMembers
  Visibility: public export
record Namespace : Type
  Namespace ::
      namespace identifier { NamespaceMembers } ;

  Totality: total
  Visibility: public export
  Constructor: 
MkNamespace : ExtAttributeList -> Identifier -> NamespaceMembers -> Namespace

  Projections:
  
.attributes : Namespace -> ExtAttributeList
  
.members : Namespace -> NamespaceMembers
  
.name : Namespace -> Identifier

  Hints:
  
Eq Namespace
  
HasAttributes Namespace
  
Show Namespace
.attributes : Namespace -> ExtAttributeList
  Visibility: public export
attributes : Namespace -> ExtAttributeList
  Visibility: public export
.name : Namespace -> Identifier
  Visibility: public export
name : Namespace -> Identifier
  Visibility: public export
.members : Namespace -> NamespaceMembers
  Visibility: public export
members : Namespace -> NamespaceMembers
  Visibility: public export
record Typedef : Type
  Typedef ::
      typedef TypeWithExtendedAttributes identifier ;

  Totality: total
  Visibility: public export
  Constructor: 
MkTypedef : ExtAttributeList -> ExtAttributeList -> IdlType -> Identifier -> Typedef

  Projections:
  
.attributes : Typedef -> ExtAttributeList
  
.name : Typedef -> Identifier
  
.type : Typedef -> IdlType
  
.typeAttributes : Typedef -> ExtAttributeList

  Hints:
  
Eq Typedef
  
HasAttributes Typedef
  
Show Typedef
.attributes : Typedef -> ExtAttributeList
  Visibility: public export
attributes : Typedef -> ExtAttributeList
  Visibility: public export
.typeAttributes : Typedef -> ExtAttributeList
  Visibility: public export
typeAttributes : Typedef -> ExtAttributeList
  Visibility: public export
.type : Typedef -> IdlType
  Visibility: public export
type : Typedef -> IdlType
  Visibility: public export
.name : Typedef -> Identifier
  Visibility: public export
name : Typedef -> Identifier
  Visibility: public export
record PDictionary : Type
  PartialDictionary ::
      dictionary identifier { DictionaryMembers } ;

  Totality: total
  Visibility: public export
  Constructor: 
MkPDictionary : ExtAttributeList -> Identifier -> DictionaryMembers -> PDictionary

  Projections:
  
.attributes : PDictionary -> ExtAttributeList
  
.members : PDictionary -> DictionaryMembers
  
.name : PDictionary -> Identifier

  Hints:
  
Eq PDictionary
  
HasAttributes PDictionary
  
Show PDictionary
.attributes : PDictionary -> ExtAttributeList
  Visibility: public export
attributes : PDictionary -> ExtAttributeList
  Visibility: public export
.name : PDictionary -> Identifier
  Visibility: public export
name : PDictionary -> Identifier
  Visibility: public export
.members : PDictionary -> DictionaryMembers
  Visibility: public export
members : PDictionary -> DictionaryMembers
  Visibility: public export
record PInterface : Type
  PartialInterfaceRest ::
      identifier { PartialInterfaceMembers } ;

  Totality: total
  Visibility: public export
  Constructor: 
MkPInterface : ExtAttributeList -> Identifier -> PartialInterfaceMembers -> PInterface

  Projections:
  
.attributes : PInterface -> ExtAttributeList
  
.members : PInterface -> PartialInterfaceMembers
  
.name : PInterface -> Identifier

  Hints:
  
Eq PInterface
  
HasAttributes PInterface
  
Show PInterface
.attributes : PInterface -> ExtAttributeList
  Visibility: public export
attributes : PInterface -> ExtAttributeList
  Visibility: public export
.name : PInterface -> Identifier
  Visibility: public export
name : PInterface -> Identifier
  Visibility: public export
.members : PInterface -> PartialInterfaceMembers
  Visibility: public export
members : PInterface -> PartialInterfaceMembers
  Visibility: public export
record PMixin : Type
  MixinRest ::
      mixin identifier { MixinMembers } ;

  Totality: total
  Visibility: public export
  Constructor: 
MkPMixin : ExtAttributeList -> Identifier -> MixinMembers -> PMixin

  Projections:
  
.attributes : PMixin -> ExtAttributeList
  
.members : PMixin -> MixinMembers
  
.name : PMixin -> Identifier

  Hints:
  
Eq PMixin
  
HasAttributes PMixin
  
Show PMixin
.attributes : PMixin -> ExtAttributeList
  Visibility: public export
attributes : PMixin -> ExtAttributeList
  Visibility: public export
.name : PMixin -> Identifier
  Visibility: public export
name : PMixin -> Identifier
  Visibility: public export
.members : PMixin -> MixinMembers
  Visibility: public export
members : PMixin -> MixinMembers
  Visibility: public export
record PNamespace : Type
  Namespace ::
      namespace identifier { NamespaceMembers } ;

  Totality: total
  Visibility: public export
  Constructor: 
MkPNamespace : ExtAttributeList -> Identifier -> NamespaceMembers -> PNamespace

  Projections:
  
.attributes : PNamespace -> ExtAttributeList
  
.members : PNamespace -> NamespaceMembers
  
.name : PNamespace -> Identifier

  Hints:
  
Eq PNamespace
  
HasAttributes PNamespace
  
Show PNamespace
.attributes : PNamespace -> ExtAttributeList
  Visibility: public export
attributes : PNamespace -> ExtAttributeList
  Visibility: public export
.name : PNamespace -> Identifier
  Visibility: public export
name : PNamespace -> Identifier
  Visibility: public export
.members : PNamespace -> NamespaceMembers
  Visibility: public export
members : PNamespace -> NamespaceMembers
  Visibility: public export
DefTypes : List Type
  Visibility: public export
PartTypes : List Type
  Visibility: public export
Definition : Type
  Definition ::
      CallbackOrInterfaceOrMixin
      Namespace
      Partial
      Dictionary
      Enum
      Typedef
      IncludesStatement
  CallbackOrInterfaceOrMixin ::
      callback CallbackRestOrInterface
      interface InterfaceOrMixin
  
  InterfaceOrMixin ::
      InterfaceRest
      MixinRest

  Visibility: public export
0 Definitions : Type
  Visibility: public export
Part : Type
  PartialDefinition ::
      interface PartialInterfaceOrPartialMixin
      PartialDictionary
      Namespace
  
  PartialInterfaceOrPartialMixin ::
      PartialInterfaceRest
      MixinRest

  Visibility: public export
accumNs : List (NS I ts) -> NP List ts
  Visibility: public export
0 PartOrDef : Type
  Visibility: public export
0 PartsAndDefs : Type
  Visibility: public export
defs : PartsAndDefs -> Definitions
  Visibility: public export
record Domain : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkDomain : String -> List Callback -> List CallbackInterface -> List Dictionary -> List Enum -> List Includes -> List Interface -> List Mixin -> List Namespace -> List Typedef -> Domain

  Projections:
  
.callbackInterfaces : Domain -> List CallbackInterface
  
.callbacks : Domain -> List Callback
  
.dictionaries : Domain -> List Dictionary
  
.domain : Domain -> String
  
.enums : Domain -> List Enum
  
.includeStatements : Domain -> List Includes
  
.interfaces : Domain -> List Interface
  
.mixins : Domain -> List Mixin
  
.namespaces : Domain -> List Namespace
  
.typedefs : Domain -> List Typedef

  Hints:
  
Eq Domain
  
HasAttributes Domain
  
Show Domain
.domain : Domain -> String
  Visibility: public export
domain : Domain -> String
  Visibility: public export
.callbacks : Domain -> List Callback
  Visibility: public export
callbacks : Domain -> List Callback
  Visibility: public export
.callbackInterfaces : Domain -> List CallbackInterface
  Visibility: public export
callbackInterfaces : Domain -> List CallbackInterface
  Visibility: public export
.dictionaries : Domain -> List Dictionary
  Visibility: public export
dictionaries : Domain -> List Dictionary
  Visibility: public export
.enums : Domain -> List Enum
  Visibility: public export
enums : Domain -> List Enum
  Visibility: public export
.includeStatements : Domain -> List Includes
  Visibility: public export
includeStatements : Domain -> List Includes
  Visibility: public export
.interfaces : Domain -> List Interface
  Visibility: public export
interfaces : Domain -> List Interface
  Visibility: public export
.mixins : Domain -> List Mixin
  Visibility: public export
mixins : Domain -> List Mixin
  Visibility: public export
.namespaces : Domain -> List Namespace
  Visibility: public export
namespaces : Domain -> List Namespace
  Visibility: public export
.typedefs : Domain -> List Typedef
  Visibility: public export
typedefs : Domain -> List Typedef
  Visibility: public export
toDomains : List (String, PartsAndDefs) -> List Domain
  Visibility: export