X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcexpr2pres_hashtbl.ml;h=79c9943c9985fc3b9839a3aa823a10e2701d2eba;hb=0cb045e7fe606a61ff725a2408684bb390bcb50c;hp=676b55dc4755d82783ff44a04d3f8c07eaa726b2;hpb=48d41935cc96e8898cc5e3da98a1706294b7b411;p=helm.git diff --git a/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml b/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml index 676b55dc4..79c9943c9 100644 --- a/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml +++ b/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml @@ -214,6 +214,27 @@ Hashtbl.add C2P.symbol_table "not" (unary P.Mtext([],"(");P.Mo([],Netconversion.ustring_of_uchar `Enc_utf8 0xAC); cexpr2pres a;P.Mtext([],")")]))); +(* inv *) +Hashtbl.add C2P.symbol_table "inv" (unary + (fun a ~priority ~assoc ~tail attr sattr -> + P.Msup([], + P.Mrow([],[ + P.Mtext([],"("); + cexpr2pres a; + P.Mtext([],")")]), + P.Mrow([],[ + P.Mo([],"-"); + P.Mn([],"1")])))); + +(* opp *) +Hashtbl.add C2P.symbol_table "opp" (unary + (fun a ~priority ~assoc ~tail attr sattr -> + P.Mrow([],[ + P.Mo([],"-"); + P.Mtext([],"("); + cexpr2pres a; + P.Mtext([],")")]))); + (* leq *) Hashtbl.add C2P.symbol_table "leq" (binary (fun a b ~priority ~assoc ~tail aattr sattr ->