vm.fail
Alpha equivalence checker for arbitrary lambda terms
1type t =
2 | Var of string
3 | Lam of string * t
4 | App of t * t
5 | Subst of string * t * t
6
7module SSet : Set.S with type elt = string
8
9val free_variables : t -> SSet.t
10val free_variable_list : t -> string list
11val pretty : t -> string
12val push_subst : string -> t -> t -> t
13val normalise : t -> t
14val normalise_counted : t -> t * int * int
15val to_named : t -> Named.t
16val of_named : Named.t -> t
17val alpha_equivalent : t -> t -> bool
18val alpha_equivalent_susp : t -> t -> bool
19val alpha_equivalent_counted : t -> t -> bool * int * int
20val substitute : string -> t -> t -> t
21val convert_from_named : Named.t -> t
22val convert_to_named : t -> Named.t