src/nbe/Syntax.ml


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

type t = Data.syn =
  | Var of int
  | Pi of Ident.local * t * (* BINDS *) t
  | Lam of Ident.local * (* BINDS *) t
  | App of t * t
  | Sg of Ident.local * t * (* BINDS *) t
  | Pair of t * t
  | Fst of t
  | Snd of t
  | Type
  | Bool
  | True
  | False
  | BoolElim of {
      motive_var : Ident.local;
      motive : (* BINDS *) t;
      true_case : t;
      false_case : t;
      scrut : t;
    }