Text.WebIDL.Types.Member

Definitions

record Const : Type

  Const ::
      const ConstType identifier = ConstValue ;
  
  ConstValue ::
      BooleanLiteral
      FloatLiteral
      integer

Totality: total
Visibility: public export
Constructor: 

MkConst : ConstType -> Identifier -> ConstValue -> Const

Projections:

.name : Const -> Identifier

.type : Const -> ConstType

.value : Const -> ConstValue

Hints:

Eq Const

HasAttributes Const

Show Const

.type : Const -> ConstType

Visibility: public export

type : Const -> ConstType

Visibility: public export

.name : Const -> Identifier

Visibility: public export

name : Const -> Identifier

Visibility: public export

.value : Const -> ConstValue

Visibility: public export

value : Const -> ConstValue

Visibility: public export

record OperationName : Type

  OperationName ::
      OperationNameKeyword
      identifier
  
  OperationNameKeyword ::
      includes

Totality: total
Visibility: public export
Constructor: 

MkOpName : String -> OperationName

Projection: 

.value : OperationName -> String

Hints:

Eq OperationName

HasAttributes OperationName

Show OperationName

.value : OperationName -> String

Visibility: public export

value : OperationName -> String

Visibility: public export

data Special : Type

  Special ::
      getter
      setter
      deleter

Totality: total
Visibility: public export
Constructors:

Getter : Special

Setter : Special

Deleter : Special

Hints:

Eq Special

HasAttributes Special

Show Special

record Op : Type -> Type

  RegularOperation ::
      Type OperationRest
  
  OperationRest ::
      OptionalOperationName ( ArgumentList ) ;
  
  OptionalOperationName ::
      OperationName
      ε
  
  SpecialOperation ::
      Special RegularOperation
  
  Operation ::
      RegularOperation
      SpecialOperation

Totality: total
Visibility: public export
Constructor: 

MkOp : a -> IdlType -> Maybe OperationName -> ArgumentList -> Op a

Projections:

.args : Op a -> ArgumentList

.name : Op a -> Maybe OperationName

.special : Op a -> a

.type : Op a -> IdlType

Hints:

Eq a => Eq (Op a)

HasAttributes a => HasAttributes (Op a)

Show a => Show (Op a)

.special : Op a -> a

Visibility: public export

special : Op a -> a

Visibility: public export

.type : Op a -> IdlType

Visibility: public export

type : Op a -> IdlType

Visibility: public export

.name : Op a -> Maybe OperationName

Visibility: public export

name : Op a -> Maybe OperationName

Visibility: public export

.args : Op a -> ArgumentList

Visibility: public export

args : Op a -> ArgumentList

Visibility: public export

0 RegularOperation : Type

Visibility: public export

0 SpecialOperation : Type

Visibility: public export

0 Operation : Type

Visibility: public export

regToOp : RegularOperation -> Operation

Visibility: public export

specToOp : SpecialOperation -> Operation

Visibility: public export

0 CallbackInterfaceMember : Type

  CallbackInterfaceMember ::
      Const
      RegularOperation

Visibility: public export

0 CallbackInterfaceMembers : Type

  CallbackInterfaceMembers ::
      ExtendedAttributeList CallbackInterfaceMember CallbackInterfaceMembers
      ε

Visibility: public export

0 Inheritance : Type

  Inheritance ::
      : identifier
      ε

Visibility: public export

data DictionaryMemberRest : Type

  DictionaryMemberRest ::
      required TypeWithExtendedAttributes identifier ;
      Type identifier Default ;

Totality: total
Visibility: public export
Constructors:

Required : ExtAttributeList -> IdlType -> Identifier -> DictionaryMemberRest

Optional : IdlType -> Identifier -> Default -> DictionaryMemberRest

Hints:

Eq DictionaryMemberRest

HasAttributes DictionaryMemberRest

Show DictionaryMemberRest

0 DictionaryMember : Type

  DictionaryMember ::
      ExtendedAttributeList DictionaryMemberRest

Visibility: public export

0 DictionaryMembers : Type

  DictionaryMembers ::
      DictionaryMember DictionaryMembers
      ε

Visibility: public export

record Readonly : Type -> Type

Totality: total
Visibility: public export
Constructor: 

MkRO : a -> Readonly a

Projection: 

.value : Readonly a -> a

Hints:

Eq a => Eq (Readonly a)

HasAttributes a => HasAttributes (Readonly a)

Show a => Show (Readonly a)

.value : Readonly a -> a

Visibility: public export

value : Readonly a -> a

Visibility: public export

record Inherit : Type -> Type

Totality: total
Visibility: public export
Constructor: 

MkI : a -> Inherit a

Projection: 

.value : Inherit a -> a

Hints:

Eq a => Eq (Inherit a)

HasAttributes a => HasAttributes (Inherit a)

Show a => Show (Inherit a)

.value : Inherit a -> a

Visibility: public export

value : Inherit a -> a

Visibility: public export

record AttributeName : Type

  AttributeName ::
      AttributeNameKeyword
      identifier
  
  AttributeNameKeyword ::
      async
      required

Totality: total
Visibility: public export
Constructor: 

MkAttributeName : String -> AttributeName

Projection: 

.value : AttributeName -> String

Hints:

Eq AttributeName

HasAttributes AttributeName

Ord AttributeName

Show AttributeName

.value : AttributeName -> String

Visibility: public export

value : AttributeName -> String

Visibility: public export

record Attribute : Type

  AttributeRest ::
      attribute TypeWithExtendedAttributes AttributeName ;

Totality: total
Visibility: public export
Constructor: 

MkAttribute : ExtAttributeList -> IdlType -> AttributeName -> Attribute

Projections:

.attrs : Attribute -> ExtAttributeList

.name : Attribute -> AttributeName

.type : Attribute -> IdlType

Hints:

Eq Attribute

HasAttributes Attribute

Show Attribute

.attrs : Attribute -> ExtAttributeList

Visibility: public export

attrs : Attribute -> ExtAttributeList

Visibility: public export

.type : Attribute -> IdlType

Visibility: public export

type : Attribute -> IdlType

Visibility: public export

.name : Attribute -> AttributeName

Visibility: public export

name : Attribute -> AttributeName

Visibility: public export

record Maplike : Type

  ReadWriteMaplike ::
      MaplikeRest
  
  MaplikeRest ::
      maplike < TypeWithExtendedAttributes , TypeWithExtendedAttributes > ;

Totality: total
Visibility: public export
Constructor: 

MkMaplike : Attributed IdlType -> Attributed IdlType -> Maplike

Projections:

.fstTpe : Maplike -> Attributed IdlType

.sndTpe : Maplike -> Attributed IdlType

Hints:

Eq Maplike

HasAttributes Maplike

HasAttributes Maplike

Show Maplike

.fstTpe : Maplike -> Attributed IdlType

Visibility: public export

fstTpe : Maplike -> Attributed IdlType

Visibility: public export

.sndTpe : Maplike -> Attributed IdlType

Visibility: public export

sndTpe : Maplike -> Attributed IdlType

Visibility: public export

record Setlike : Type

  ReadWriteSetlike ::
      SetlikeRest
  
  SetlikeRest ::
      setlike < TypeWithExtendedAttributes > ;

Totality: total
Visibility: public export
Constructor: 

MkSetlike : Attributed IdlType -> Setlike

Projection: 

.type : Setlike -> Attributed IdlType

Hints:

Eq Setlike

HasAttributes Setlike

Show Setlike

.type : Setlike -> Attributed IdlType

Visibility: public export

type : Setlike -> Attributed IdlType

Visibility: public export

0 Stringifier : Type

  StringifierRest ::
      OptionalReadOnly AttributeRest
      RegularOperation
      ;
  
  Stringifier ::
      stringifier StringifierRest

Visibility: public export

0 StaticMember : Type

  StaticMember ::
      static StaticMemberRest
  
  StaticMemberRest ::
      OptionalReadOnly AttributeRest
      RegularOperation

Visibility: public export

0 NamespaceMember : Type

  NamespaceMember ::
      RegularOperation
      readonly AttributeRest

Visibility: public export

0 NamespaceMembers : Type

  NamespaceMembers ::
      ExtendedAttributeList NamespaceMember NamespaceMembers
      ε

Visibility: public export

record Constructor : Type

  Constructor ::
      constructor ( ArgumentList ) ;

Totality: total
Visibility: public export
Constructor: 

MkConstructor : ArgumentList -> Constructor

Projection: 

.args : Constructor -> ArgumentList

Hints:

Eq Constructor

HasAttributes Constructor

Show Constructor

.args : Constructor -> ArgumentList

Visibility: public export

args : Constructor -> ArgumentList

Visibility: public export

data PartialInterfaceMember : Type

  PartialInterfaceMember ::
      Const
      Operation
      Stringifier
      StaticMember
      Iterable
      AsyncIterable
      ReadOnlyMember
      ReadWriteAttribute
      ReadWriteMaplike
      ReadWriteSetlike
      InheritAttribute
  
  Iterable ::
      iterable < TypeWithExtendedAttributes OptionalType > ;

Totality: total
Visibility: public export
Constructors:

IConst : Const -> PartialInterfaceMember

IOp : Operation -> PartialInterfaceMember

IStr : Stringifier -> PartialInterfaceMember

IStatic : StaticMember -> PartialInterfaceMember

IAttr : Attribute -> PartialInterfaceMember

IMap : Maplike -> PartialInterfaceMember

ISet : Setlike -> PartialInterfaceMember

IAttrRO : Readonly Attribute -> PartialInterfaceMember

IMapRO : Readonly Maplike -> PartialInterfaceMember

ISetRO : Readonly Setlike -> PartialInterfaceMember

IAttrInh : Inherit Attribute -> PartialInterfaceMember

IIterable : Attributed IdlType -> OptionalType -> PartialInterfaceMember

IAsync : Attributed IdlType -> OptionalType -> ArgumentList -> PartialInterfaceMember

Hints:

Eq PartialInterfaceMember

HasAttributes PartialInterfaceMember

Show PartialInterfaceMember

data MixinMember : Type

  MixinMember ::
      Const
      RegularOperation
      Stringifier
      OptionalReadOnly AttributeRest

Totality: total
Visibility: public export
Constructors:

MConst : Const -> MixinMember

MOp : RegularOperation -> MixinMember

MStr : Stringifier -> MixinMember

MAttr : Attribute -> MixinMember

MAttrRO : Readonly Attribute -> MixinMember

Hints:

Eq MixinMember

HasAttributes MixinMember

Show MixinMember

0 PartialInterfaceMembers : Type

  PartialInterfaceMembers ::
      ExtendedAttributeList PartialInterfaceMember PartialInterfaceMembers
      ε

Visibility: public export

0 InterfaceMember : Type

  InterfaceMember ::
      PartialInterfaceMember
      Constructor

Visibility: public export

0 InterfaceMembers : Type

  InterfaceMembers ::
      ExtendedAttributeList InterfaceMember InterfaceMembers
      ε

Visibility: public export

0 MixinMembers : Type

  MixinMembers ::
      ExtendedAttributeList MixinMember MixinMembers
      ε

Visibility: public export

const : Attributed CallbackInterfaceMember -> Maybe Const

Visibility: export

optional : DictionaryMember -> Maybe Attribute

Visibility: export

required : DictionaryMember -> Maybe Attribute

Visibility: export

part : (PartialInterfaceMember -> Maybe a) -> Attributed InterfaceMember -> Maybe a

Visibility: export

const : Attributed MixinMember -> Maybe Const

Visibility: export

attrRO : Attributed MixinMember -> Maybe (Readonly Attribute)

Visibility: export

attr : Attributed MixinMember -> Maybe Attribute

Visibility: export

attrRO : NamespaceMember -> Maybe (Readonly Attribute)

Visibility: export

const : PartialInterfaceMember -> Maybe Const

Visibility: export

attrRO : PartialInterfaceMember -> Maybe (Readonly Attribute)

Visibility: export

attr : PartialInterfaceMember -> Maybe Attribute

Visibility: export