Term.cppo.ml 699 Bytes
Newer Older
1 2 3
open AlphaLib
open BindingForms

4 5 6 7
#define tele ('bn, 'fn) tele
#define term ('bn, 'fn) term

type tele =
8
  | TeleNil
9
  | TeleCons of 'bn binder * term outer * tele rebind
10

11
and term =
12
  | TVar of 'fn
13 14 15
  | TPi  of (tele, term) bind
  | TLam of (tele, term) bind
  | TApp of term * term list
16
[@@deriving visitors { variety = "iter"; ancestors = ["BindingForms.iter"]; public = ["visit_term"] },
17
            visitors { variety = "map"; ancestors = ["BindingForms.map"]; public = ["visit_term"] },
18
            visitors { variety = "endo"; ancestors = ["BindingForms.endo"]; public = ["visit_term"] },
19
            visitors { variety = "iter2"; ancestors = ["BindingForms.iter2"]; public = ["visit_term"] }]