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"]) *)