View constructors reference

This is the exhaustive reference for the view vocabulary. Start with Views for conceptual grounding; come here for exact signatures, render semantics, and the gaps each constructor closed.

The view types

Three levels, same structure:

Type	Typed message?	Serializable?	Use case
`View Msg`	Yes, fully	No	Authoring with type safety; `reflectView` converts to `RView`
`Ui Msg`	Yes, fully	No	Simple proof specs; minimal vocabulary
`RView`	No, defunctionalized	Yes	The emitted, runtime-ready form

Minimal vocabulary

The original closed set. Every app uses at least these.

Constructor (Lean)	Signature	Renders as	Notes
`text`	`String → RView`	Static text content	A text node with no wrapper element
`scalar`	`String → RView`	Live scalar value	The current value of a named scalar field; re-renders on change
`rowField`	`String → RView`	Current row's field	Used only inside a `list` item view; reads `current_row[field_name]`
`input`	`String → RView`	Text input two-way bound	Bound to a named scalar; emits `oninput` handler without re-render
`button`	`String → String → Atom → RView`	Clickable button	`button label tag payload` fires `step(tag, payload)` on click
`list`	`String → RView → RView`	Table iterator	`list table item_view` renders `item_view` once per row; row context active for `rowField`
`col`	`List RView → RView`	Container `<div>`	Groups children; sets up grid layout context

Styled vocabulary

These carry inline CSS, so an entire product surface — chrome, shells, every screen — is UI-as-data with no hand-written render code downstream.

Constructor (Lean)	Signature	Renders as	Notes
`raw`	`String → RView`	Bare text node	No wrapper element; the text is emitted directly
`el`	`String → String → List RView → RView`	Custom element	`el tag style children` — an arbitrary HTML element with inline `style` attribute
`img`	`String → String → RView`	`<img>` tag	`img src style` — source URL and inline CSS
`styled`	`String → RView → RView`	Wrapped node	`styled style child` wraps a single child with an inline style
`btn`	`String → String → String → Atom → RView`	Styled button	`btn label style tag payload` — carries inline style; fires `step(tag, payload)` on click
`click`	`String → String → Atom → List RView → RView`	Clickable container	`click style tag payload children` — a styled `<div>` firing `step(tag, payload)` with the scalar payload, not the row
`rowSelect`	`String → String → List RView → RView`	Clickable list item	Closes gap G1: fires `step(tag, ROW)` with the whole current row as payload, so handlers can lift row fields to scalars with `setFromRow` (conversation selection, contact picking, etc.)
`inp`	`String → String → String → RView`	Styled input	`inp field placeholder style` — text input with inline CSS, two-way bound to a named scalar field
`rowFieldOr`	`String → String → RView`	Row field or fallback	`rowFieldOr key fallback` renders the row field, or the literal `fallback` string if the field is absent — used inside `list`

Lists and derived views

Render subsets or projections of a table without filtering the table itself.

Constructor (Lean)	Signature	Renders as	Notes
`listWhere`	`String → String → String → RView → RView`	Filtered list	Closes gap G2: `listWhere table field scalarKey item` renders `item` once per row where `row[field] == scalars[scalarKey]`. Keeps the full table intact; the view is the filter. Example: show messages for a selected conversation without modifying the `messages` table.
`listDistinct`	`String → String → RView → RView`	Grouped list	Closes gap G3: `listDistinct table field item` renders `item` once per distinct value of `field`, using the latest row with that value. Canonical for conversation lists and grouped feeds where you want one item per sender or per thread.
`listOrEmpty`	`String → RView → RView → RView`	Conditional table	Closes gap G11: `listOrEmpty table item empty` renders `item` once per row of `table`, or the `empty` view when the table is empty. Essential because empty states are real screens users see; a framework without this pushes authors into hand-written conditionals.

Conditionals

Branch on scalar or row-field values. Keep state-changing logic in handlers; keep appearance-changing logic here.

Constructor (Lean)	Signature	Renders as	Notes
`cond`	`String → RView → RView → RView`	Truthiness branch	`cond scalarKey then else` branches on whether `scalars[key]` is truthy (non-null, non-false, non-zero, non-empty string)
`condEq`	`String → String → RView → RView → RView`	Equality branch	Closes gap G7: `condEq scalarKey value then else` branches on `scalars[key] == value`. Example: `condEq "chat_type" "group" group_view dm_view`
`condField`	`String → RView → RView → RView`	Row field truthiness	`condField field then else` branches on the current row's `field` — used inside `list` items. Example: show "read" indicator only if the message is read.
`condFieldEqScalar`	`String → String → RView → RView → RView`	Row-to-scalar equality	Closes gap G16: `condFieldEqScalar field scalarKey then else` branches on `row[field] == scalars[key]`. The canonical way to express "is this message mine?" as `condFieldEqScalar "from" "identity" own_style others_style`, because outgoing detection is `from == identity`

Advanced: arbitrary attributes and SVG

Constructor (Lean)	Signature	Renders as	Notes
`elAttr`	`String → List (String × String) → List RView → RView`	Element with attributes	Closes gap G10: `elAttr tag attrs children` renders an HTML element with arbitrary `(key, value)` attributes and children. The only constructor with an `svg:` namespaced attribute becomes an SVG element, enabling line-art icons as data. Example: `elAttr "svg" [("svg:viewBox", "0 0 24 24"), ("svg:xmlns", "http://www.w3.org/2000/svg")] [elAttr "path" [("d", "M12 2L22 20H2Z")] []]` renders an SVG triangle.

`Ui` — the minimal proven vocabulary

A simpler, four-constructor algebra used for proof specs and proof-tier view assertions.

inductive Ui (Msg : Type) where
  | text   : String → Ui Msg            -- static text
  | bind   : String → Ui Msg            -- render a named scalar
  | button : String → Msg → Ui Msg      -- button label and typed message
  | col    : List (Ui Msg) → Ui Msg     -- container

Constructor	Renders	Use in proofs
`text`	Static text	A fixed string assertion
`bind`	Live scalar value	Assert that a scalar exists and render its value
`button`	Clickable button	Assert that a handler fires
`col`	Container	Group children

Ui is intentionally minimal: the proof tier cares only about the message-bearing control points and their labels. Styling, layout, and derived views are the reflected (RView) layer's responsibility.

`ViewDsl` — authoring helpers

Generic aliases for RView constructors, shared by every app. These are thin wrapping functions with no proof impact — they are pure syntactic convenience.

namespace Encapp.ViewDsl
open Encapp
 
abbrev V := RView
 
def box (style : String) (cs : List V) : V := 
  .el "div" style cs
 
def span (style text : String) : V := 
  .el "span" style [.raw text]
 
def txt (style text : String) : V := 
  .el "div" style [.raw text]
 
def fld (key fallback : String) : V := 
  .rowFieldOr key fallback
 
def navTo (label style path : String) : V := 
  .btn label style "nav" (.str path)
 
def goTo (style path : String) (cs : List V) : V := 
  .click style "nav" (.str path) cs
 
def selectRow (style tag : String) (cs : List V) : V := 
  .rowSelect style tag cs
 
def scalar (k : String) : V := 
  .scalar k

Helper	Maps to	Use case
`box style children`	`el "div" style children`	A styled container div
`span style text`	`el "span" style [raw text]`	A styled inline text span
`txt style text`	`el "div" style [raw text]`	A styled block text div
`fld key fallback`	`rowFieldOr key fallback`	Render row field with literal fallback
`navTo label style path`	`btn label style "nav" (.str path)`	Navigate to `path` on click (fires the `nav` handler)
`goTo style path children`	`click style "nav" (.str path) children`	Clickable container that navigates
`selectRow style tag children`	`rowSelect style tag children`	Row-selecting list item (fires row payload)
`scalar k`	`.scalar k`	Render live scalar value

The nav handler is conventional — it sets the path scalar to navigate between pages. See Routing and gates.

View reflection and defunctionalization

reflectView : View Msg → RView converts authored View Msg (with typed Msg values) to serializable RView (with (tag, payload) pairs). The conversion is mechanical:

Every Msg value is defunctionalized to its tag : String and payload : Atom
Structure is preserved: an el in the source is an el in the output
All type safety is discharged at compile time

def reflectView : View Msg → RView

You use this when authoring a typed view : Model → View HMsg function. For mostly-layout screens with little typed logic, author directly in RView with ViewDsl helpers.

Rendering

The interpreter that runs the app is the interpreter that proves the test. Each platform has a renderer:

appDomJs (web) — maps every RView constructor to a DOM node; wires events to step
appRnJs (React Native) — maps the same constructors to RN elements

Both consume the identical appCoreJs state machine. test/native-core-identity.mjs asserts byte-identity of the two emitted cores. Style handling differs — web takes inline CSS directly, native parses them into RN style objects — which is why emitNative accepts base-style parameters for normalization.

Recap

Minimal vocabulary (text, scalar, rowField, input, button, list, col) is the foundation
Styled vocabulary adds inline CSS so UI-as-data covers the entire product
Derived view constructors (listWhere, listDistinct, listOrEmpty, conditionals) close specific gaps without extending the table algebra
elAttr is the escape hatch for arbitrary attributes and SVG
ViewDsl provides thin helpers over RView for common patterns
Ui is the proof-tier, minimal algebra; RView is the emitted form

Next steps

Views guide — conceptual overview and use patterns
App model — how to author view : Model → View Msg functions
Effects — the handler side of interaction