]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/virtuals.mli
basic_rg: reduction was not tail recursive by mistake
[helm.git] / helm / software / matita / virtuals.mli
1 type symbol = Glib.unichar
2 type tag = string
3
4 val add_virtual: string list -> symbol -> tag list -> unit
5
6 exception Not_a_virtual
7 val symbol_of_virtual: string -> string * symbol
8
9 val get_all_virtuals : unit -> (tag * (string list * symbol) list) list
10
11 val add_eqclass: symbol list -> unit
12 val similar_symbols: symbol -> symbol list
13
14 val get_all_eqclass: unit -> symbol list list
15
16 (* (["\\lambda";"\\"], "λ", ["logics";"letters"]) *)