open Bwd

type t = Data.value =
  | Neutral of ne
  | Pi of Ident.local * t * clo
  | Lam of Ident.local * clo
  | Sg of Ident.local * 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 {
      motive_var : Ident.local;
      motive : clo;
      true_case : t;
      false_case: t;
    }

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

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