index.ml (562B)
1 (* Pairs of indices, which we usualy denote ij or (i, j). The first index i is 2 * a de Bruijn index in the usual sense; it refers to a binder, with the 3 * innermost binder being 0. All our binders are multibinders (i.e., they bind 4 * multiple variables simultaneously), so each entry in an environment is 5 * actually a range of variables, and the second index j refers to a variable 6 * within such a range. *) 7 8 type index = Of of int * int 9 type t = index 10 11 let pp_print 12 : Format.formatter -> index -> unit 13 = fun ppf (Of (i, j)) -> 14 Format.fprintf ppf "%d.%d" i j