open Bwd

type value =
  | Neutral of ne
  | Pi of value * clos
  | Lam of clos
  | Sg of value * clos
  | Pair of value * value
  | Type
  | Bool
  | True
  | False

and ne = ne_head * frame bwd
and ne_head = Var of int (* De Bruijn levels *)
and frame = 
  | BoolElim of {
      cmot: clos;
      vtrue: value;
      vfalse: value;
    }
  | App of value
  | Fst
  | Snd

and env = value bwd
and clos = Clos of { body : Syntax.tm; env : env }