helm/software/lambda-delta/basic_rg/brg.ml

   1 module U = NUri
   2 module A = Aut
   3
   4 type uri = U.uri
   5 type id = A.id
   6
   7 type binder = Abst | Abbr
   8
   9 type term = Sort of int
  10           | LRef of int
  11           | GRef of uri
  12           | Cast of term * term
  13           | Appl of term * term
  14           | Bind of id * binder * term * term
  15