type 'nf i_n_var_ = [ `N of int | 'nf i_var_ ]
type 'nf i_num_var_ =
[ `I of int * 'nf Listx.listx
- | `Match of 'nf i_num_var_ * int * (int * 'nf) list ref * 'nf list
+ | `Match of 'nf i_num_var_ * int * int * (int * 'nf) list ref * 'nf list
| `N of int
| `Var of int ]
type 'nf nf_ =
[ `I of int * 'nf Listx.listx
- | `Lam of bool * 'nf nf_
- | `Match of 'nf i_num_var_ * int * (int * 'nf) list ref * 'nf list
+ | `Lam of bool * int * 'nf nf_
+ | `Match of 'nf i_num_var_ * int * int * (int * 'nf) list ref * 'nf list
| `N of int
| `Var of int ]
type nf = nf nf_
val mk_app : nf -> nf -> nf
val mk_appl : nf -> nf list -> nf
val mk_appx : nf -> nf Listx.listx -> nf
-val mk_match : nf i_num_var_ -> int -> (int * nf) list ref -> nf list -> nf
+val mk_match : nf i_num_var_ -> int -> int -> (int * nf) list ref -> nf list -> nf
val subst : bool -> int -> nf -> nf -> nf
val parse' : string list -> nf list * string list
val eta_compare : nf -> nf -> int