The app model

An Encapp app is authored in two faces and proven identical. This guide walks the complete hello example (Encapp/Examples/Hello.lean, 177 lines) top to bottom, because it exercises every piece: routing, an identity handshake, a composer, two tables and a proof.

1. State — a `Doc`

def helloInit : Doc where
  scalars := [ ("identity", .null), ("path", .str "/connect"), ("draft", .str "") ]
  tables  := [ ("messages", []), ("my_messages", []) ]

Doc is named scalars plus named tables of rows. path is a scalar like any other — routing is ordinary state, not a special mechanism. See Encapp.Doc.

2. Messages — a real inductive

inductive HMsg where
  | connect : String → HMsg     -- wallet pubkey
  | input   : String → HMsg     -- new draft value
  | submit  : HMsg              -- post the draft
  | nav     : String → HMsg     -- route to a path
  deriving DecidableEq, Inhabited

This is the ergonomic win over stringly-typed handlers: a button carries a typed message, and a typo is a type error.

3. The typed view

def helloView (d : Doc) : View HMsg :=
  match asStr (d.getScalar "path") with
  | "/connect"  => .col [ .text "Connect your wallet to use Hello.",
                          .button "Connect" (.connect "79be667ef9dcbbac") ]
  | "/feed"     => .col [ .list "messages" (.rowField "body"),
                          .input "draft", .button "Post" .submit,
                          .button "My posts →" (.nav "/my_posts") ]
  | "/my_posts" => .col [ .list "my_messages" (.rowField "body"),
                          .input "draft", .button "Post" .submit,
                          .button "← Feed" (.nav "/feed") ]
  | _           => .text ""

Note what routing is not: there is no route constructor in the view vocabulary. Dispatching on a scalar keeps the language small and puts the routing decision in one readable place.

.list tbl item renders item once per row of tbl; inside it, .rowField k reads the current row.

4. The typed update

def helloApp : App Doc HMsg where
  init := helloInit
  update msg d := match msg with
    | .connect w => ((d.setScalar "identity" (.str w)).setScalar "path" (.str "/feed"), [])
    | .input v   => (d.setScalar "draft" (.str v), [])
    | .submit    =>
        let d' := ((d.appendRow "messages" (postRow d)).appendRow "my_messages" (postRow d))
                    .setScalar "draft" .null
        (d', [ .submit { id := short16 (asStr (d.getScalar "identity"))
                       , data := asStr (d.getScalar "draft") } ])
    | .nav p     => (d.setScalar "path" (.str p), [])
  view := helloView

update returns (newModel, effects). Effects are data — Cmd.submit describes a store write; it does not perform one. What executes it is chosen downstream and is related to the spec by proof.

5. Reflection — the same app as data

Codegen cannot walk functions, so the app is projected to a ReflApp.

Messages become tags:

def encodeMsg : HMsg → String × Atom
  | .connect w => ("connect", .str w)
  | .input v   => ("set:draft", .str v)
  | .submit    => ("submit", .null)
  | .nav p     => ("nav", .str p)

update becomes a handler table:

def helloHandlers : List RHandler :=
  [ ⟨"connect",   [ .setInput "identity", .setConst "path" (.str "/feed") ]⟩,
    ⟨"set:draft", [ .setInput "draft" ]⟩,
    ⟨"submit",    [ .pushDraft "messages", .pushDraft "my_messages",
                    .setConst "draft" .null ]⟩,
    ⟨"nav",       [ .setInput "path" ]⟩ ]

Each handler is a tag plus a list of Eff values applied in order.

The view becomes one RView per page:

def helloPages : List (String × RView) :=
  ["/connect", "/feed", "/my_posts"].map
    (fun p => (p, reflectView (helloView (helloInit.setScalar "path" (.str p)))))

reflectView is a mechanical translation from View HMsg to RView that defunctionalizes each button's message through encodeMsg.

The reflected app:

def helloReflected : ReflApp Unit where
  init     := helloInit
  pages    := helloPages
  handlers := helloHandlers

The type parameter is the host binding. Unit means "this app expects nothing of its host" — a pure view app.

6. The theorem that keeps them honest

Two faces would be two things to maintain, and they would drift. So they are tied:

def demo : List HMsg :=
  [ .connect "79be667ef9dcbbac", .input "hello from node:test", .submit ]
 
def demoSteps : List (String × Payload) :=
  [ ("connect",   .atom (.str "79be667ef9dcbbac"))
  , ("set:draft", .atom (.str "hello from node:test"))
  , ("submit",    .atom .null) ]
 
def helloFinal : Doc := helloApp.ofMsgLog demo
 
theorem hello_reflected_matches :
    reflRun helloHandlers demoSteps helloInit = helloFinal := by
  native_decide

If a handler stops mirroring the typed update, this fails at lake build.

7. Prove what the app must do

Ordinary facts about the app are ordinary theorems:

theorem hello_draft_cleared : helloFinal.getScalar "draft" = .null := by native_decide
theorem hello_one_message   : (helloFinal.rows "messages").length = 1 := by native_decide

View bindings can be proven too — this catches a whole class of copy-paste bug where a page lists the wrong table:

theorem helloView_feed_lists_messages :
    firstListTable (helloView (helloInit.setScalar "path" (.str "/feed")))
      = some "messages" := by native_decide

For user stories rather than single facts, use the workflow DSL, which gives you the proof and the cross-platform test corpus from one definition.

8. Emit

def main : IO Unit := do
  let html := AppGen.emit (DocChrome.light "Hello") helloReflected
  IO.FS.createDirAll "dist"
  IO.FS.writeFile "dist/index.html" html

lean_exe «helloapp» where
  root := `HelloApp

and run lake exe helloapp. See Web for what emit produces, and Native / Desktop for the other two targets.

Authoring shortcuts

Encapp/ViewDsl.lean provides app-agnostic sugar so styled trees stay readable:

open Encapp.ViewDsl
 
box "display:flex;gap:8px" [
  txt  "font-size:20px;font-weight:600" "Inbox",
  span "color:#888" "3 unread",
  navTo "Settings" "padding:8px" "/settings"
]

Helper	Builds
`box style children`	a styled `div`
`span style text` / `txt style text`	styled inline / block text
`scalar k`	the live value of a scalar
`fld key fallback`	a row field with a literal fallback
`navTo label style path`	a button that fires the conventional `nav` handler
`goTo style path children`	a clickable container that navigates
`selectRow style tag children`	a list item that fires `tag` with the whole row as payload

The nav* helpers assume the conventional "nav" handler that sets the path scalar.

Recap

Apps are authored in two faces: a typed View Msg + update for ergonomics, and a reflected RView + handlers for codegen and proof.
State is a Doc: named scalars plus named tables of rows. Routing is a scalar like any other.
Messages are real inductive types, not strings. Typos become type errors.
Handlers are data: a tag plus a list of effects applied in order.
Theorems prove that the two faces produce identical results, keeping them from drifting.
Apps emit to web, native, and desktop platforms with one command.

Next steps

Views — the closed RView vocabulary and how each constructor renders
Effects — the Eff algebra and domain-free vs. messaging-shaped operations
Workflows — testing your app with cross-platform assertions