ColonelJ

Inductive bvec (T : Set) : nat -> Set :=
  | BLeaf : T -> bvec T 0
  | BNode log2len : bvec T log2len -> bvec T log2len -> bvec T (S log2len).

Definition bvec_leaf T (v : bvec T 0) := let 'BLeaf a := v in a.
Definition bvec_l T n (v : bvec T (S n)) := let 'BNode n l _ := v in l.
Definition bvec_r T n (v : bvec T (S n)) := let 'BNode n _ r := v in r.

Fixpoint zip (T U V : Set) (f : T -> U -> V) n (u : bvec T n) :=
  match u in bvec _ n return bvec U n -> bvec V n with

ColonelJ

import Window
 
main : Signal Element
main = display <~ Window.dimensions
 
display (w, h) = flow down [width w <| centered txt1, width w <| centered txt2]
 
txt1 = toText "Reeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeally long string"
txt2 = toText "Hello world"