# LeanUI templates
LeanUI views are values of type `Html Msg`. They can be built with the smart constructors of
`LeanUI.Html` (`el`, `text`, `Attr.*`), or written as JSX-style templates:
```lean
module
public import LeanUI
meta import LeanUI.Syntax -- templates are compile-time only
public section
open LeanUI
def item (t : Todo) (editing : Bool) : Html Msg :=
.toggle t.id} />
```
A template is an ordinary Lean term. It is type-checked like the code it stands for, it can appear
wherever an `Html Msg` can, and Lean expressions go inside `{…}`.
Contents: [setup and cost](#setup-and-cost) · [elements](#elements) ·
[attributes](#attributes) · [events](#events) · [children and text](#children-and-text) ·
[fragments](#fragments) · [components](#components) · [namespaces](#namespaces-svg-and-mathml) ·
[where templates can appear](#where-templates-can-appear) · [errors](#errors-and-warnings) ·
[grammar](#grammar) · [limitations](#limitations) · [how it works](#how-it-works)
## Setup and cost
Add `meta import LeanUI.Syntax` to a module that writes templates. Nothing else is needed: the
syntax is active in that module only (modules importing it do not see it, and need their own
`meta import` to write templates).
The import is `meta` because templates cost nothing at run time. `LeanUI.Syntax` and the Lean
compiler it is built on run while your module compiles and are never linked into the program. A
template expands to the constructors you would write by hand (`Html.elem`, `Html.text`,
`Attr.attr`, `Attr.prop`, `Attr.key`, the `Attr.on*` helpers, array literals, `toString`); every
decision that depends on the type of an interpolated value is made by the elaborator, not by a
type class at run time. The example above expands to
```lean
Html.elem Ns.html "li"
#[Attr.key (toString t.id),
Attr.attr "class" (("todo" ++ if t.done then " completed" else "") ++ if editing then " editing" else "")]
#[Html.elem Ns.html "input"
#[Attr.attr "class" "toggle", Attr.attr "type" "checkbox", Attr.prop "checked" (PropValue.bool t.done),
Attr.onCheck fun _ => Msg.toggle t.id] #[],
Html.elem Ns.html "label" #[Attr.onDblClick (Msg.edit t.id)] #[Html.text t.title],
Html.elem Ns.html "button"
(let xs := #[Attr.attr "class" "destroy", Attr.onClick (Msg.remove t.id)];
if editing then xs.push (Attr.attr "disabled" "") else xs) #[]]
```
Measured on `examples/Counter.lean`, which is written as a template:
- the generated C is the same as for the hand-written view except for the numbering of constants;
its runtime initializer calls `Init` and `LeanUI` only, and the file mentions no `Lean.*` and no
`LeanUI.Syntax` declaration (checked by `leanui-syntax-tests`);
- the wasm64 build is 1,034,481 bytes (hand-written: 1,034,487), and the browser test
`tests/browser/counter.mjs` sends the same 7 flushes, 279 commands and 1,250 bytes in Chromium
and Firefox;
- the native test binary that uses templates links no compiler code (about 1.9 MB; a runtime
`import Lean` would add about 100 MB).
## Elements
```lean
…
-- element with children
-- self-closing
-- custom elements (with a dash) are fine
```
- The `<` must touch the tag name: `, found `.
- Void elements (`area base br col embed hr img input link meta source track wbr`) cannot have
children: write ` `, ``.
- Tag names are case-sensitive and are emitted as written (SVG needs `linearGradient`,
`foreignObject`, …). A name starting with an uppercase letter is a [component](#components).
- An unknown lowercase HTML element without a dash gets a warning (`` is probably a typo); so
does an unknown SVG or MathML element inside `