vm.fail
Alpha equivalence checker for arbitrary lambda terms
1type t =
2 | BVar of int
3 | FVar of string
4 | Lam of t
5 | App of t * t
6
7module SSet : Set.S with type elt = string
8
9exception Not_locally_closed
10
11val free_variables : t -> SSet.t
12val free_variable_list : t -> string list
13val pretty : t -> string
14val open_at : int -> string -> t -> t
15val open_top : t -> string -> t
16val close_at : int -> string -> t -> t
17val close_top : t -> string -> t
18val lc : t -> bool
19val require_lc : t -> unit
20val subst_bvar : int -> t -> t -> t
21val subst_fvar : string -> t -> t -> t
22val substitute : string -> t -> t -> t
23val convert_from_named : Named.t -> t
24val convert_to_named : t -> Named.t
25val alpha_equivalent : t -> t -> bool
26val alpha_equivalent_counted : t -> t -> bool * int * int
27val normalise : t -> t
28val normalise_counted : t -> t * int * int