Example 02 / Try it

Every state gets a place.

Choose a state to see what the ticket list shows. Try Empty and Failure: they tell two different stories.

Live componentLEAN + REACT

These controls select example states. They do not make network requests.

From the blog post.lean

import LeanReact
open LeanReact

def ticketList (state : ResourceState (Array String) String) : Element :=
  match state with
  | .idle => DOM.p {} #[text "Loading tickets…"]
  | .loading _ => DOM.p {} #[text "Loading tickets…"]
  | .failure _ (.loader message) =>
      DOM.p { role := some "alert" } #[text message]
  | .failure _ (.exception _) =>
      DOM.p { role := some "alert" } #[text "Could not load tickets. Try again."]
  | .success _ titles =>
      if titles.isEmpty then
        DOM.p {} #[text "No open tickets. You're all caught up."]
      else
        DOM.ul {} (titles.map fun title => DOM.li {} #[text title])

Empty is a successful request with no tickets. Failure means we could not load them. The same match handles both.