Text.SVG.Tag

Definitions

data HasHref : String -> Type

  Proof that the given element can have an `href` attribute

Totality: total
Visibility: public export
Constructors:

HasHrefImage : HasHref "image"

HasHrefPattern : HasHref "pattern"

HasHrefUse : HasHref "use"

data HasCX : String -> Type

  Proof that the given element can have a `cx` attribute

Totality: total
Visibility: public export
Constructors:

HasCXCircle : HasCX "circle"

HasCXEllipse : HasCX "ellipse"

data HasCY : String -> Type

  Proof that the given element can have a `cy` attribute

Totality: total
Visibility: public export
Constructors:

HasCYCircle : HasCY "circle"

HasCYEllipse : HasCY "ellipse"

data HasRX : String -> Type

  Proof that the given element can have an `rx` attribute

Totality: total
Visibility: public export
Constructors:

HasRXEllipse : HasRX "ellipse"

HasRXRect : HasRX "rect"

data HasRY : String -> Type

  Proof that the given element can have an `ry` attribute

Totality: total
Visibility: public export
Constructors:

HasRYEllipse : HasRY "ellipse"

HasRYRect : HasRY "rect"

data HasX : String -> Type

  Proof that the given element can have an `x` attribute

Totality: total
Visibility: public export
Constructors:

HasXFilter : HasX "filter"

HasXImage : HasX "image"

HasXRect : HasX "rect"

HasXText : HasX "text"

data HasY : String -> Type

  Proof that the given element can have a `y` attribute

Totality: total
Visibility: public export
Constructors:

HasYFilter : HasY "filter"

HasYImage : HasY "image"

HasYRect : HasY "rect"

HasYText : HasY "text"

data HasHeight : String -> Type

  Proof that the given element can have a `height` attribute

Totality: total
Visibility: public export
Constructors:

HasHeightFilter : HasHeight "filter"

HasHeightImage : HasHeight "image"

HasHeightMask : HasHeight "mask"

HasHeightPath : HasHeight "path"

HasHeightPattern : HasHeight "pattern"

HasHeightRect : HasHeight "rect"

HasHeightSVG : HasHeight "svg"

HasHeightUse : HasHeight "use"

data HasFill : String -> Type

  Proof that the given element can have a `fill` attribute

Totality: total
Visibility: public export
Constructors:

HasFillCircle : HasFill "circle"

HasFillEllipse : HasFill "ellipse"

HasFillGroup : HasFill "g"

HasFillLine : HasFill "line"

HasFillPath : HasFill "path"

HasFillPolygon : HasFill "polygon"

HasFillPolyline : HasFill "polyline"

HasFillRect : HasFill "rect"

HasFillSVG : HasFill "svg"

HasFillText : HasFill "text"

data HasStroke : String -> Type

  Proof that the given element can have a `stroke` attribute

Totality: total
Visibility: public export
Constructors:

HasStrokeCircle : HasStroke "circle"

HasStrokeEllipse : HasStroke "ellipse"

HasStrokeGroup : HasStroke "g"

HasStrokeLine : HasStroke "line"

HasStrokePath : HasStroke "path"

HasStrokePolygon : HasStroke "polygon"

HasStrokePolyline : HasStroke "polyline"

HasStrokeRect : HasStroke "rect"

HasStrokeSVG : HasStroke "svg"

HasStrokeText : HasStroke "text"

data HasWidth : String -> Type

  Proof that the given element can have a `width` attribute

Totality: total
Visibility: public export
Constructors:

HasWidthFilter : HasWidth "filter"

HasWidthImage : HasWidth "image"

HasWidthMask : HasWidth "mask"

HasWidthPath : HasWidth "path"

HasWidthPattern : HasWidth "pattern"

HasWidthRect : HasWidth "rect"

HasWidthSVG : HasWidth "svg"

HasWidthUse : HasWidth "use"

data HasViewBox : String -> Type

  Proof that the given element can have a `viewPort` attribute

Totality: total
Visibility: public export
Constructors:

HasViewBoxMarker : HasViewBox "marker"

HasViewBoxPattern : HasViewBox "pattern"

HasViewBoxSVG : HasViewBox "svg"

HasViewBoxSymbol : HasViewBox "symbol"

HasViewBoxView : HasViewBox "view"

data HasPoints : String -> Type

  Proof that the given element can have a `points` attribute

Totality: total
Visibility: public export
Constructors:

HasPointsPolygon : HasPoints "polygon"

HasPointsPolyline : HasPoints "polyline"

data IsText : String -> Type

  Proof that the given element displays some text

Totality: total
Visibility: public export
Constructors:

IsTextText : IsText "text"

IsTextTSpan : IsText "tspan"

IsTextGroup : IsText "g"

IsTextSVG : IsText "svg"