module T = Term

type lvl = Lvl of int

type closure = C of env * T.term

and env = value list

and value
  = Type
  | T0
  | T1
  | T1vl
  | TNat
  | Suc   of value
  | Zero
  | TBool
  | True
  | False
  | Pi    of value * closure
  | Lam   of closure
  | Sg    of value * closure
  | Pair  of value * value
  | Stuck of stuck * value (* second arg is type *)

and stuck
  = Var  of lvl
  | Ind0 of closure * stuck
  | Ind1 of closure * value * stuck
  | IndN of closure * value * closure * stuck
  | IndB of closure * value * value * stuck
  | App  of stuck * value * value (* fn; val; type of fn *)
  | Fst  of stuck
  | Snd  of stuck