open Bwd

type t = Data.value =
  | Neutral of ne
  | Pi of t * clo
  | Lam of clo
  | Sg of t * clo
  | Pair of t * t
  | Type
  | Bool
  | True
  | False

and ne = Data.ne
and ne_head = Data.ne_head = Var of int (* De Bruijn levels *)
and frm = Data.frm =
  | App of t
  | Fst
  | Snd
  | BoolElim of {
      cmot: clo;
      vtrue: t;
      vfalse: t;
    }

and env = Data.env
and clo = Data.clo = Clo of { body : Data.syn; env : env }

let var i = Neutral (Var i, Bwd.Emp)