Commit 21d89337 authored by POTTIER Francois's avatar POTTIER Francois

Removed the conversions to de Bruijn indices.

parent af5a3da3
......@@ -82,13 +82,6 @@ type raw_term =
type nominal_term =
(Atom.t, Atom.t) term
(* A de Bruijn term is one where free name occurrences are represented as a
de Bruijn index and binding name occurrences carry no information. This
definition is used for illustrative purposes only. *)
type debruijn_term =
(int, unit) term
(* -------------------------------------------------------------------------- *)
__COPY
......@@ -130,26 +123,6 @@ let fa' : nominal_term -> Atom.Set.t =
(* -------------------------------------------------------------------------- *)
(* Conversions from raw terms and from nominal terms to de Bruijn terms. *)
class raw2debruijn = object
inherit [_] map
inherit [_] KitToDeBruijn.String.map
end
let raw2debruijn : KitToDeBruijn.String.env -> raw_term -> debruijn_term =
new raw2debruijn # visit_term
class nominal2debruijn = object
inherit [_] map
inherit [_] KitToDeBruijn.Atom.map
end
let nominal2debruijn : KitToDeBruijn.Atom.env -> nominal_term -> debruijn_term =
new nominal2debruijn # visit_term
(* -------------------------------------------------------------------------- *)
(* [subst] applies a substitution to a nominal term, yielding a nominal term. *)
(* A substitution is a finite map of atoms to nominal terms. *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment