Main: IO(Unit)
  IO {
    IO.print("Hello, world!")
  }

// A 'Hello, world!"
Main: IO(Unit)
  IO {
    IO.print("Hello, world!")
  }

// Quicksort (using recursion)
quicksort(list: List<Nat>): List<Nat>
  case list {
    nil:
      []
    cons:
      fst = list.head
      min = filter!((x) x <? list.head, list.tail)
      max = filter!((x) x >=? list.head, list.tail)
      quicksort(min) ++ [fst] ++ quicksort(max)
  }

// List iteration (using folds)
some_text: String
  List.foldl!!("",
    (str, result) 
      str = String.to_upper(str)
      str = String.reverse(str)
      result | str,
    ["cba","fed","ihg"])

// List iteration (using fors)
some_text: String
  result = ""
  for str in ["cba","fed","ihg"] with result:
    str = String.to_upper(str)
    str = String.reverse(str)
    result | str
  result

// A boolean
type Bool {
  true
  false
}

// A natural number
type Nat {
  zero
  succ(pred: Nat)
}

// A polymorphic list
type List <A: Type> {
  nil
  cons(head: A, tail: List<A>)
}

// A polymorphic pair
type Pair <A: Type, B: Type> {
  new(fst: A, snd: B)
}

// A polymorphic dependent pair
type Sigma <A: Type, B: A -> Type> {
  new(fst: A, snd: B(fst))
}

// A polymorphic list with a statically known size
type Vector <A: Type> ~ (size: Nat) {
  nil                                              ~ (size = 0) 
  cons(size: Nat, head: Nat, tail: Vector<A,size>) ~ (size = 1 + size)
}

// A bounded natural number
type Fin ~ <lim: Nat> {
  zero<N: Nat>               ~ (lim = Nat.succ(N))
  succ<N: Nat>(pred: Fin<N>) ~ (lim = Nat.succ(N))
}

// The type used in equality proofs
type Equal <A: Type, a: A> ~ (b: A) {
  refl ~ (b = a)
}

// A burrito
type Monad <M: Type -> Type> {
  new(
    bind: <A: Type, B: Type> M<A> -> (A -> M<B>) -> M<B>
    pure: <A: Type> A -> M<A>
  )
}

// Some game entity
type Entity {
  player(
    name: String
    pos: V3
    health: Nat
    items: List<Item>
    sprite: Image
  )
  wall(
    hitbox: Pair<V3, V3>
    collision: Entity -> Entity
    sprite: Image
  )
}

// Proof that `a == a + 0`
Nat.add.zero(a: Nat): a == Nat.add(a, 0)
  case a {
    zero: refl
    succ: apply(Nat.succ, Nat.add.zero(a.pred))
  }!

// Proof that `1 + (a + b) == a + (1 + b)`
Nat.add.succ(a: Nat, b: Nat): Nat.succ(a + b) == (a + Nat.succ(b))
  case a {
    zero: refl
    succ: apply(Nat.succ, Nat.add.succ(a.pred, b))
  }!

// Proof that addition is commutative
Nat.add.comm(a: Nat, b: Nat): (a + b) == (b + a)
  case a {
    zero:
      Nat.add.zero(b)
    succ: 
      p0 = Nat.add.succ(b, a.pred)
      p1 = Nat.add.comm(b, a.pred)
      p0 :: rewrite X in Nat.succ(X) == _ with p1
  }!

// Render function
App.Hello.draw: App.Draw<App.Hello.State>
  (state)
  <div style={"border": "1px solid black"}>
    <div style={"font-weight": "bold"}>"Hello, world!"</div>
    <div>"Clicks: " | Nat.show(state@local)</div>
    <div>"Visits: " | Nat.show(state@global)</div>
  </div>

// Event handler
App.Hello.when: App.When<App.Hello.State>
  (event, state)
  case event {
    init: IO {
      App.watch!(App.room_zero)
      App.new_post!(App.room_zero, App.empty_post)
    }
    mouse_down: IO {
      App.set_local!(state@local + 1)
    }
  } default App.pass!