Commit 569ddc71 by POTTIER Francois

Forgot to include [rename_term] in [ToolboxOutput].

parent 068b44ae
......@@ -212,3 +212,6 @@ module Map = struct
fold (fun _ v accu -> Set.union (f v) accu) m Set.empty
end
type renaming =
atom Map.t
......@@ -65,3 +65,6 @@ module Map : sig
val codomain: ('a -> Set.t) -> 'a t -> Set.t
end
type renaming =
atom Map.t
......@@ -34,41 +34,8 @@ module Make (Term : INPUT) = struct
#include "AlphaLibMacros.cppo.ml"
__FA
FA(term)
__FILTER
FILTER(term)
__BA
BA(term)
__AVOIDS
AVOIDS(term)
__GUQ
GUQ(term)
__COPY
COPY(term)
__AVOID
AVOID(term)
__IMPORT
IMPORT(term)
__EXPORT
EXPORT(term)
__SHOW
SHOW(term)
__SIZE
SIZE(term)
__EQUIV
EQUIV(term)
__ALL
ALL(term)
(* Mnemonic: Substitute for variables in terms. *)
__SUBST(TVar)
......
......@@ -106,6 +106,11 @@ module type OUTPUT = sig
val equiv_term: nominal_term -> nominal_term -> bool
(* [rename_term] applies a renaming to the free atoms of a nominal term,
yielding a nominal term. *)
val rename_term: Atom.renaming -> nominal_term -> nominal_term
(* [subst_TVar_term] applies a substitution to a nominal term, yielding a
nominal term. This is a substitution of things for variables; in the
general case, [TVar] could be a constructor of some type [thing] other
......
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