module FF.HTML.Spec.Safe.Syntax where

open import Agda.Builtin.String using (String)
open import Cubical.Data.List.Base using (List; []; _∷_)
import FF.CSS.Spec.Safe as CSS

open import FF.HTML.Core using (Attribute; attr; node)
open import FF.HTML.Spec.Safe public

el : (tagName : TagName) -> List (Attribute spec tagName) -> List HtmlT -> HtmlT
el = node

el₀ : TagName -> List HtmlT -> HtmlT
el₀ tagName children = node tagName [] children

infix 1 ‹_❴_❵›_‹/›
infix 1 ‹_›_‹/›
infix 1 ⟨_❴_❵⟩_⟨/⟩
infix 1 ⟨_∣_⟩_⟨/⟩

-- Agda reserves ⦃ and ⦄ for instance arguments. The ornamental
-- brackets ❴ and ❵ give the same visual role without invoking instances.
‹_❴_❵›_‹/› : (tagName : TagName) -> List (Attribute spec tagName) -> List HtmlT -> HtmlT
‹ tagName ❴ attrs ❵› children ‹/› = el tagName attrs children

‹_›_‹/› : TagName -> List HtmlT -> HtmlT
‹ tagName › children ‹/› = el₀ tagName children

⟨_❴_❵⟩_⟨/⟩ : (tagName : TagName) -> List (Attribute spec tagName) -> List HtmlT -> HtmlT
⟨ tagName ❴ attrs ❵⟩ children ⟨/⟩ = el tagName attrs children

⟨_∣_⟩_⟨/⟩ : (tagName : TagName) -> List (Attribute spec tagName) -> List HtmlT -> HtmlT
⟨ tagName ∣ attrs ⟩ children ⟨/⟩ = el tagName attrs children

div : TagName
div = divTag

html : TagName
html = htmlTag

head : TagName
head = headTag

title-tag : TagName
title-tag = titleTag

body : TagName
body = bodyTag

meta : TagName
meta = metaTag

p : TagName
p = pTag

span : TagName
span = spanTag

section : TagName
section = sectionTag

header : TagName
header = headerTag

main : TagName
main = mainTag

nav : TagName
nav = navTag

h1 : TagName
h1 = h1Tag

h2 : TagName
h2 = h2Tag

a : TagName
a = aTag

button : TagName
button = buttonTag

ul : TagName
ul = ulTag

li : TagName
li = liTag

input : TagName
input = inputTag

select : TagName
select = selectTag

option : TagName
option = optionTag

textarea : TagName
textarea = textareaTag

link-tag : TagName
link-tag = linkTag

script : TagName
script = scriptTag

template : TagName
template = templateTag

audio : TagName
audio = audioTag

video : TagName
video = videoTag

iframe : TagName
iframe = iframeTag

fencedframe : TagName
fencedframe = fencedframeTag

object : TagName
object = objectTag

area : TagName
area = areaTag

source : TagName
source = sourceTag

track : TagName
track = trackTag

caption : TagName
caption = captionTag

table : TagName
table = tableTag

tbody : TagName
tbody = tbodyTag

tr : TagName
tr = trTag

td : TagName
td = tdTag

th : TagName
th = thTag

hr : TagName
hr = hrTag

details : TagName
details = detailsTag

dialog : TagName
dialog = dialogTag

geolocation : TagName
geolocation = geolocationTag

summary : TagName
summary = summaryTag

slot : TagName
slot = slotTag

form : TagName
form = formTag

label : TagName
label = labelTag

img : TagName
img = imgTag

image-map : TagName
image-map = imageMapTag

class : {tagName : TagName} -> String -> Attribute spec tagName
class value = attr classAttr (tokens value)

id : {tagName : TagName} -> String -> Attribute spec tagName
id value = attr idAttr value

title : {tagName : TagName} -> String -> Attribute spec tagName
title value = attr titleAttr value

style : {tagName : TagName} -> String -> Attribute spec tagName
style value = attr styleAttr (styleRaw value)

style-decl : {tagName : TagName} -> CSS.DeclarationT -> Attribute spec tagName
style-decl declaration = attr styleAttr (styleOne declaration)

style-decls : {tagName : TagName} -> InlineStyle -> Attribute spec tagName
style-decls value = attr styleAttr value

style-cons : CSS.DeclarationT -> InlineStyle -> InlineStyle
style-cons = styleCons

popover : {tagName : TagName} -> Popover -> Attribute spec tagName
popover value = attr popoverAttr value

data- : {tagName : TagName} -> String -> String -> Attribute spec tagName
data- key value = attr (dataAttr key) value

aria- : {tagName : TagName} -> String -> String -> Attribute spec tagName
aria- key value = attr (ariaAttr key) value

href : String -> Attribute spec aTag
href value = attr (hrefAttr hrefA) (url value)

target : Target -> Attribute spec aTag
target value = attr (targetAttr targetA) value

rel : String -> Attribute spec aTag
rel value = attr (relAttr relA) (relTokens value)

rel-keyword : RelToken -> Attribute spec aTag
rel-keyword value = attr (relAttr relA) (relOne value)

rel-keywords : RelList -> Attribute spec aTag
rel-keywords value = attr (relAttr relA) value

a-type : String -> Attribute spec aTag
a-type value = attr (typeAttr mimeA) (mime value)

interestfor : String -> Attribute spec aTag
interestfor value = attr (interestforAttr interestA) (idRef value)

a-attributionsrc : AttributionSrc -> Attribute spec aTag
a-attributionsrc value = attr (attributionsrcAttr attributionA) value

a-shape : AreaShape -> Attribute spec aTag
a-shape value = attr (shapeAttr shapeA) value

src : String -> Attribute spec imgTag
src value = attr (srcAttr srcImg) (url value)

alt : String -> Attribute spec imgTag
alt value = attr (altAttr altImg) value

img-attributionsrc : AttributionSrc -> Attribute spec imgTag
img-attributionsrc value = attr (attributionsrcAttr attributionImg) value

img-loading : Loading -> Attribute spec imgTag
img-loading value = attr (loadingAttr loadingImg) value

img-fetchpriority : FetchPriority -> Attribute spec imgTag
img-fetchpriority value = attr (fetchpriorityAttr fetchPriorityImg) value

img-usemap : String -> Attribute spec imgTag
img-usemap value = attr (usemapAttr usemapImg) (idRef value)

img-ismap : Attribute spec imgTag
img-ismap = attr ismapAttr present

link-as : LinkAs -> Attribute spec linkTag
link-as value = attr asAttr value

link-href : String -> Attribute spec linkTag
link-href value = attr (hrefAttr hrefLink) (url value)

link-rel : String -> Attribute spec linkTag
link-rel value = attr (relAttr relLink) (relTokens value)

link-rel-keyword : RelToken -> Attribute spec linkTag
link-rel-keyword value = attr (relAttr relLink) (relOne value)

link-rel-keywords : RelList -> Attribute spec linkTag
link-rel-keywords value = attr (relAttr relLink) value

link-media : String -> Attribute spec linkTag
link-media value = attr (mediaAttr mediaLink) (mediaQuery value)

link-imagesizes : String -> Attribute spec linkTag
link-imagesizes value = attr imagesizesAttr (sizes value)

link-imagesrcset : String -> Attribute spec linkTag
link-imagesrcset value = attr imagesrcsetAttr (srcset value)

link-blocking : Blocking -> Attribute spec linkTag
link-blocking value = attr (blockingAttr blockingLink) value

link-fetchpriority : FetchPriority -> Attribute spec linkTag
link-fetchpriority value = attr (fetchpriorityAttr fetchPriorityLink) value

link-crossorigin : CrossOrigin -> Attribute spec linkTag
link-crossorigin value = attr (crossoriginAttr corsLink) value

link-integrity : String -> Attribute spec linkTag
link-integrity value = attr (integrityAttr integrityLink) (integrity value)

link-type : String -> Attribute spec linkTag
link-type value = attr (typeAttr mimeLink) (mime value)

link-disabled : Attribute spec linkTag
link-disabled = attr (disabledAttr disableLink) present

meta-charset : String -> Attribute spec metaTag
meta-charset value = attr charsetAttr value

meta-name : String -> Attribute spec metaTag
meta-name value = attr (nameAttr nameMeta) value

meta-content : String -> Attribute spec metaTag
meta-content value = attr contentAttr value

meta-media : String -> Attribute spec metaTag
meta-media value = attr (mediaAttr mediaMeta) (mediaQuery value)

http-equiv : String -> Attribute spec metaTag
http-equiv value = attr httpEquivAttr value

script-src : String -> Attribute spec scriptTag
script-src value = attr (srcAttr srcScript) (url value)

script-type : ScriptKind -> Attribute spec scriptTag
script-type value = attr scriptTypeAttr value

script-blocking : Blocking -> Attribute spec scriptTag
script-blocking value = attr (blockingAttr blockingScript) value

script-attributionsrc : AttributionSrc -> Attribute spec scriptTag
script-attributionsrc value = attr (attributionsrcAttr attributionScript) value

script-fetchpriority : FetchPriority -> Attribute spec scriptTag
script-fetchpriority value = attr (fetchpriorityAttr fetchPriorityScript) value

script-async : Attribute spec scriptTag
script-async = attr asyncAttr present

script-defer : Attribute spec scriptTag
script-defer = attr deferAttr present

script-crossorigin : CrossOrigin -> Attribute spec scriptTag
script-crossorigin value = attr (crossoriginAttr corsScript) value

script-integrity : String -> Attribute spec scriptTag
script-integrity value = attr (integrityAttr integrityScript) (integrity value)

audio-src : String -> Attribute spec audioTag
audio-src value = attr (srcAttr srcAudio) (url value)

audio-controls : Attribute spec audioTag
audio-controls = attr (controlsAttr mediaAudio) present

audio-autoplay : Attribute spec audioTag
audio-autoplay = attr (autoplayAttr mediaAudio) present

audio-loop : Attribute spec audioTag
audio-loop = attr (loopAttr mediaAudio) present

audio-muted : Attribute spec audioTag
audio-muted = attr (mutedAttr mediaAudio) present

audio-controlslist : String -> Attribute spec audioTag
audio-controlslist value = attr (controlslistAttr mediaAudio) (controlsTokens value)

audio-controlslist-keyword : ControlsListToken -> Attribute spec audioTag
audio-controlslist-keyword value = attr (controlslistAttr mediaAudio) (controlsOne value)

audio-controlslist-keywords : ControlsList -> Attribute spec audioTag
audio-controlslist-keywords value = attr (controlslistAttr mediaAudio) value

audio-disableremoteplayback : Attribute spec audioTag
audio-disableremoteplayback = attr (disableremoteplaybackAttr mediaAudio) present

audio-loading : Loading -> Attribute spec audioTag
audio-loading value = attr (loadingAttr loadingAudio) value

audio-preload : Preload -> Attribute spec audioTag
audio-preload value = attr (preloadAttr mediaAudio) value

audio-crossorigin : CrossOrigin -> Attribute spec audioTag
audio-crossorigin value = attr (crossoriginAttr corsAudio) value

video-src : String -> Attribute spec videoTag
video-src value = attr (srcAttr srcVideo) (url value)

video-controls : Attribute spec videoTag
video-controls = attr (controlsAttr mediaVideo) present

video-autoplay : Attribute spec videoTag
video-autoplay = attr (autoplayAttr mediaVideo) present

video-loop : Attribute spec videoTag
video-loop = attr (loopAttr mediaVideo) present

video-muted : Attribute spec videoTag
video-muted = attr (mutedAttr mediaVideo) present

video-controlslist : String -> Attribute spec videoTag
video-controlslist value = attr (controlslistAttr mediaVideo) (controlsTokens value)

video-controlslist-keyword : ControlsListToken -> Attribute spec videoTag
video-controlslist-keyword value = attr (controlslistAttr mediaVideo) (controlsOne value)

video-controlslist-keywords : ControlsList -> Attribute spec videoTag
video-controlslist-keywords value = attr (controlslistAttr mediaVideo) value

video-disableremoteplayback : Attribute spec videoTag
video-disableremoteplayback = attr (disableremoteplaybackAttr mediaVideo) present

video-disablepictureinpicture : Attribute spec videoTag
video-disablepictureinpicture = attr disablepictureinpictureAttr present

video-loading : Loading -> Attribute spec videoTag
video-loading value = attr (loadingAttr loadingVideo) value

video-preload : Preload -> Attribute spec videoTag
video-preload value = attr (preloadAttr mediaVideo) value

video-poster : String -> Attribute spec videoTag
video-poster value = attr posterAttr (url value)

video-playsinline : Attribute spec videoTag
video-playsinline = attr playsinlineAttr present

input-type : InputType -> Attribute spec inputTag
input-type value = attr inputTypeAttr value

input-alpha : Attribute spec inputTag
input-alpha = attr alphaAttr present

input-switch : Attribute spec inputTag
input-switch = attr switchAttr present

input-colorspace : ColorSpace -> Attribute spec inputTag
input-colorspace value = attr colorspaceAttr value

input-name : String -> Attribute spec inputTag
input-name value = attr (nameAttr nameInput) value

input-accept : String -> Attribute spec inputTag
input-accept value = attr (acceptAttr acceptInput) value

input-usemap : String -> Attribute spec inputTag
input-usemap value = attr (usemapAttr usemapInput) (idRef value)

input-autocomplete : Autocomplete -> Attribute spec inputTag
input-autocomplete value = attr (autocompleteAttr autocompleteInput) value

input-formaction : String -> Attribute spec inputTag
input-formaction value = attr (formactionAttr overrideInput) (url value)

input-formenctype : FormEncoding -> Attribute spec inputTag
input-formenctype value = attr (formenctypeAttr overrideInput) value

input-formmethod : FormMethod -> Attribute spec inputTag
input-formmethod value = attr (formmethodAttr overrideInput) value

input-formnovalidate : Attribute spec inputTag
input-formnovalidate = attr (formnovalidateAttr overrideInput) present

input-formtarget : Target -> Attribute spec inputTag
input-formtarget value = attr (formtargetAttr overrideInput) value

input-dirname : String -> Attribute spec inputTag
input-dirname value = attr (dirnameAttr dirnameInput) value

input-popovertarget : String -> Attribute spec inputTag
input-popovertarget value = attr (popovertargetAttr popoverInput) (idRef value)

input-popovertargetaction : PopoverTargetAction -> Attribute spec inputTag
input-popovertargetaction value = attr (popovertargetactionAttr popoverInput) value

placeholder : String -> Attribute spec inputTag
placeholder value = attr (placeholderAttr placeholderInput) value

required : Attribute spec inputTag
required = attr (requiredAttr requiredInput) present

checked : Attribute spec inputTag
checked = attr checkedAttr present

button-type : ButtonType -> Attribute spec buttonTag
button-type value = attr buttonTypeAttr value

button-command : ButtonCommand -> Attribute spec buttonTag
button-command value = attr commandAttr value

button-custom-command : String -> Attribute spec buttonTag
button-custom-command suffix = button-command (customCommand (customCommandName suffix))

button-commandfor : String -> Attribute spec buttonTag
button-commandfor value = attr commandforAttr (idRef value)

button-popovertarget : String -> Attribute spec buttonTag
button-popovertarget value = attr (popovertargetAttr popoverButton) (idRef value)

button-popovertargetaction : PopoverTargetAction -> Attribute spec buttonTag
button-popovertargetaction value = attr (popovertargetactionAttr popoverButton) value

disabled-button : Attribute spec buttonTag
disabled-button = attr (disabledAttr disableButton) present

button-formaction : String -> Attribute spec buttonTag
button-formaction value = attr (formactionAttr overrideButton) (url value)

button-formenctype : FormEncoding -> Attribute spec buttonTag
button-formenctype value = attr (formenctypeAttr overrideButton) value

button-formmethod : FormMethod -> Attribute spec buttonTag
button-formmethod value = attr (formmethodAttr overrideButton) value

button-formnovalidate : Attribute spec buttonTag
button-formnovalidate = attr (formnovalidateAttr overrideButton) present

button-formtarget : Target -> Attribute spec buttonTag
button-formtarget value = attr (formtargetAttr overrideButton) value

action : String -> Attribute spec formTag
action value = attr actionAttr (url value)

accept-charset : String -> Attribute spec formTag
accept-charset value = attr acceptCharsetAttr value

form-accept : String -> Attribute spec formTag
form-accept value = attr (acceptAttr acceptForm) value

form-autocomplete : Autocomplete -> Attribute spec formTag
form-autocomplete value = attr formAutocompleteAttr value

method : FormMethod -> Attribute spec formTag
method value = attr methodAttr value

for : String -> Attribute spec labelTag
for value = attr (forAttr forLabel) (idRef value)

map-name : String -> Attribute spec imageMapTag
map-name value = attr (nameAttr nameMap) value

select-size : String -> Attribute spec selectTag
select-size value = attr selectSizeAttr value

select-autocomplete : Autocomplete -> Attribute spec selectTag
select-autocomplete value = attr (autocompleteAttr autocompleteSelect) value

select-required : Attribute spec selectTag
select-required = attr (requiredAttr requiredSelect) present

select-multiple : Attribute spec selectTag
select-multiple = attr (multipleAttr multipleSelect) present

textarea-autocomplete : Autocomplete -> Attribute spec textareaTag
textarea-autocomplete value = attr (autocompleteAttr autocompleteTextarea) value

textarea-dirname : String -> Attribute spec textareaTag
textarea-dirname value = attr (dirnameAttr dirnameTextarea) value

textarea-placeholder : String -> Attribute spec textareaTag
textarea-placeholder value = attr (placeholderAttr placeholderTextarea) value

textarea-required : Attribute spec textareaTag
textarea-required = attr (requiredAttr requiredTextarea) present

area-href : String -> Attribute spec areaTag
area-href value = attr (hrefAttr hrefArea) (url value)

area-alt : String -> Attribute spec areaTag
area-alt value = attr (altAttr altArea) value

area-coords : String -> Attribute spec areaTag
area-coords value = attr coordsAttr (coords value)

area-shape : AreaShape -> Attribute spec areaTag
area-shape value = attr (shapeAttr shapeArea) value

area-target : Target -> Attribute spec areaTag
area-target value = attr (targetAttr targetArea) value

area-rel : String -> Attribute spec areaTag
area-rel value = attr (relAttr relArea) (relTokens value)

area-rel-keyword : RelToken -> Attribute spec areaTag
area-rel-keyword value = attr (relAttr relArea) (relOne value)

area-rel-keywords : RelList -> Attribute spec areaTag
area-rel-keywords value = attr (relAttr relArea) value

area-download : String -> Attribute spec areaTag
area-download value = attr (downloadAttr downloadArea) value

object-data : String -> Attribute spec objectTag
object-data value = attr objectDataAttr (url value)

object-usemap : String -> Attribute spec objectTag
object-usemap value = attr (usemapAttr usemapObject) (idRef value)

iframe-csp : String -> Attribute spec iframeTag
iframe-csp value = attr cspAttr (csp value)

iframe-src : String -> Attribute spec iframeTag
iframe-src value = attr (srcAttr srcIframe) (url value)

iframe-loading : Loading -> Attribute spec iframeTag
iframe-loading value = attr (loadingAttr loadingIframe) value

iframe-allow : String -> Attribute spec iframeTag
iframe-allow value = attr (allowAttr allowIframe) value

iframe-sandbox : String -> Attribute spec iframeTag
iframe-sandbox value = attr sandboxAttr (sandboxTokens value)

iframe-sandbox-all : Attribute spec iframeTag
iframe-sandbox-all = attr sandboxAttr sandboxAll

iframe-sandbox-token : SandboxToken -> Attribute spec iframeTag
iframe-sandbox-token value = attr sandboxAttr (sandboxOne value)

iframe-sandbox-tokens : Sandbox -> Attribute spec iframeTag
iframe-sandbox-tokens value = attr sandboxAttr value

iframe-credentialless : Attribute spec iframeTag
iframe-credentialless = attr credentiallessAttr present

iframe-private-token : String -> Attribute spec iframeTag
iframe-private-token value = attr privateTokenAttr (privateToken value)

fencedframe-allow : String -> Attribute spec fencedframeTag
fencedframe-allow value = attr (allowAttr allowFencedframe) value

fencedframe-width : String -> Attribute spec fencedframeTag
fencedframe-width value = attr (widthAttr sizeFencedframe) value

fencedframe-height : String -> Attribute spec fencedframeTag
fencedframe-height value = attr (heightAttr sizeFencedframe) value

details-name : String -> Attribute spec detailsTag
details-name value = attr (nameAttr nameDetails) value

details-open : Attribute spec detailsTag
details-open = attr (openAttr openDetails) present

dialog-closedby : DialogClosedBy -> Attribute spec dialogTag
dialog-closedby value = attr closedbyAttr value

dialog-open : Attribute spec dialogTag
dialog-open = attr (openAttr openDialog) present

geolocation-autolocate : Attribute spec geolocationTag
geolocation-autolocate = attr autolocateAttr present

geolocation-watch : Attribute spec geolocationTag
geolocation-watch = attr watchAttr present

slot-name : String -> Attribute spec slotTag
slot-name value = attr (nameAttr nameSlot) value

th-abbr : String -> Attribute spec thTag
th-abbr value = attr abbrAttr value

legacy-align : {tagName : TagName} -> AlignElement tagName -> String -> Attribute spec tagName
legacy-align appliesTo value = attr (alignAttr appliesTo) value

legacy-background : {tagName : TagName} -> BackgroundElement tagName -> String -> Attribute spec tagName
legacy-background appliesTo value = attr (backgroundAttr appliesTo) (url value)

legacy-bgcolor : {tagName : TagName} -> BgColorElement tagName -> String -> Attribute spec tagName
legacy-bgcolor appliesTo value = attr (bgcolorAttr appliesTo) (css value)

legacy-border : {tagName : TagName} -> BorderElement tagName -> String -> Attribute spec tagName
legacy-border appliesTo value = attr (borderAttr appliesTo) value

legacy-color : {tagName : TagName} -> ColorElement tagName -> String -> Attribute spec tagName
legacy-color appliesTo value = attr (colorAttr appliesTo) (css value)

table-summary : String -> Attribute spec tableTag
table-summary value = attr summaryAttr value

template-shadowrootmode : ShadowRootMode -> Attribute spec templateTag
template-shadowrootmode value = attr shadowrootmodeAttr value

template-shadowrootserializable : Attribute spec templateTag
template-shadowrootserializable = attr shadowrootserializableAttr present

template-shadowrootslotassignment : ShadowRootSlotAssignment -> Attribute spec templateTag
template-shadowrootslotassignment value = attr shadowrootslotassignmentAttr value

divNode : List (Attribute spec divTag) -> List HtmlT -> HtmlT
divNode attrs children = node divTag attrs children

divNode₀ : List HtmlT -> HtmlT
divNode₀ children = node divTag [] children

pNode : List (Attribute spec pTag) -> List HtmlT -> HtmlT
pNode attrs children = node pTag attrs children

pNode₀ : List HtmlT -> HtmlT
pNode₀ children = node pTag [] children

spanNode : List (Attribute spec spanTag) -> List HtmlT -> HtmlT
spanNode attrs children = node spanTag attrs children

spanNode₀ : List HtmlT -> HtmlT
spanNode₀ children = node spanTag [] children

sectionNode : List (Attribute spec sectionTag) -> List HtmlT -> HtmlT
sectionNode attrs children = node sectionTag attrs children

sectionNode₀ : List HtmlT -> HtmlT
sectionNode₀ children = node sectionTag [] children

h1Node : List (Attribute spec h1Tag) -> List HtmlT -> HtmlT
h1Node attrs children = node h1Tag attrs children

h1Node₀ : List HtmlT -> HtmlT
h1Node₀ children = node h1Tag [] children

h2Node : List (Attribute spec h2Tag) -> List HtmlT -> HtmlT
h2Node attrs children = node h2Tag attrs children

h2Node₀ : List HtmlT -> HtmlT
h2Node₀ children = node h2Tag [] children

aNode : List (Attribute spec aTag) -> List HtmlT -> HtmlT
aNode attrs children = node aTag attrs children

aNode₀ : List HtmlT -> HtmlT
aNode₀ children = node aTag [] children

buttonNode : List (Attribute spec buttonTag) -> List HtmlT -> HtmlT
buttonNode attrs children = node buttonTag attrs children

buttonNode₀ : List HtmlT -> HtmlT
buttonNode₀ children = node buttonTag [] children

infix 1 ‹div❴_❵›_‹/div›
infix 1 ‹div›_‹/div›
infix 1 ‹p❴_❵›_‹/p›
infix 1 ‹p›_‹/p›
infix 1 ‹span❴_❵›_‹/span›
infix 1 ‹span›_‹/span›
infix 1 ‹section❴_❵›_‹/section›
infix 1 ‹section›_‹/section›
infix 1 ‹h1❴_❵›_‹/h1›
infix 1 ‹h1›_‹/h1›
infix 1 ‹h2❴_❵›_‹/h2›
infix 1 ‹h2›_‹/h2›
infix 1 ‹a❴_❵›_‹/a›
infix 1 ‹a›_‹/a›
infix 1 ‹button❴_❵›_‹/button›
infix 1 ‹button›_‹/button›

‹div❴_❵›_‹/div› : List (Attribute spec divTag) -> List HtmlT -> HtmlT
‹div❴ attrs ❵› children ‹/div› = divNode attrs children

‹div›_‹/div› : List HtmlT -> HtmlT
‹div› children ‹/div› = divNode₀ children

‹p❴_❵›_‹/p› : List (Attribute spec pTag) -> List HtmlT -> HtmlT
‹p❴ attrs ❵› children ‹/p› = pNode attrs children

‹p›_‹/p› : List HtmlT -> HtmlT
‹p› children ‹/p› = pNode₀ children

‹span❴_❵›_‹/span› : List (Attribute spec spanTag) -> List HtmlT -> HtmlT
‹span❴ attrs ❵› children ‹/span› = spanNode attrs children

‹span›_‹/span› : List HtmlT -> HtmlT
‹span› children ‹/span› = spanNode₀ children

‹section❴_❵›_‹/section› : List (Attribute spec sectionTag) -> List HtmlT -> HtmlT
‹section❴ attrs ❵› children ‹/section› = sectionNode attrs children

‹section›_‹/section› : List HtmlT -> HtmlT
‹section› children ‹/section› = sectionNode₀ children

‹h1❴_❵›_‹/h1› : List (Attribute spec h1Tag) -> List HtmlT -> HtmlT
‹h1❴ attrs ❵› children ‹/h1› = h1Node attrs children

‹h1›_‹/h1› : List HtmlT -> HtmlT
‹h1› children ‹/h1› = h1Node₀ children

‹h2❴_❵›_‹/h2› : List (Attribute spec h2Tag) -> List HtmlT -> HtmlT
‹h2❴ attrs ❵› children ‹/h2› = h2Node attrs children

‹h2›_‹/h2› : List HtmlT -> HtmlT
‹h2› children ‹/h2› = h2Node₀ children

‹a❴_❵›_‹/a› : List (Attribute spec aTag) -> List HtmlT -> HtmlT
‹a❴ attrs ❵› children ‹/a› = aNode attrs children

‹a›_‹/a› : List HtmlT -> HtmlT
‹a› children ‹/a› = aNode₀ children

‹button❴_❵›_‹/button› : List (Attribute spec buttonTag) -> List HtmlT -> HtmlT
‹button❴ attrs ❵› children ‹/button› = buttonNode attrs children

‹button›_‹/button› : List HtmlT -> HtmlT
‹button› children ‹/button› = buttonNode₀ children

genericWithAttrsExample : HtmlT
genericWithAttrsExample =
  ‹ div ❴ class "card" ∷ [] ❵›
    text "Hello" ∷ []
  ‹/›

genericEmptyAttrsExample : HtmlT
genericEmptyAttrsExample =
  ‹ p ›
    text "Hello" ∷ []
  ‹/›

simpleGlyphExample : HtmlT
simpleGlyphExample =
  ⟨ div ❴ class "card" ∷ [] ❵⟩
    text "Hello" ∷ []
  ⟨/⟩

namedWrapperExample : HtmlT
namedWrapperExample =
  ‹div❴ class "card" ∷ [] ❵›
    ‹p› text "Hello" ∷ [] ‹/p› ∷ []
  ‹/div›