Commit 68385317 by Martin Clochard

### Renamed transformation curry into prop_curry

parent 92eb6f5d
 ... @@ -156,7 +156,7 @@ LIB_TRANSFORM = simplify_formula inlining split_goal induction \ ... @@ -156,7 +156,7 @@ LIB_TRANSFORM = simplify_formula inlining split_goal induction \ introduction abstraction close_epsilon lift_epsilon \ introduction abstraction close_epsilon lift_epsilon \ eliminate_epsilon \ eliminate_epsilon \ eval_match instantiate_predicate smoke_detector \ eval_match instantiate_predicate smoke_detector \ reduction_engine compute induction_pr curry reduction_engine compute induction_pr prop_curry LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq pvs isabelle \ LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq pvs isabelle \ simplify gappa cvc3 yices mathematica simplify gappa cvc3 yices mathematica ... ...
 open Term open Term open Decl open Decl let rec curry t = match t.t_node with let rec curry t = match t.t_node with | Tbinop (Timplies, lhs, rhs) -> expand t lhs (curry rhs) | Tbinop (Timplies, lhs, rhs) -> expand t lhs (curry rhs) | _ -> t_map curry t | _ -> t_map curry t ... @@ -10,11 +10,10 @@ and expand orig l r = match l.t_node with ... @@ -10,11 +10,10 @@ and expand orig l r = match l.t_node with | Tbinop (Tand, a, b) -> expand orig a (expand orig b r) | Tbinop (Tand, a, b) -> expand orig a (expand orig b r) | _ -> t_label_copy orig (t_implies (curry l) r) | _ -> t_label_copy orig (t_implies (curry l) r) let curry = Trans.goal (fun pr t -> [create_prop_decl Pgoal pr (curry t)]) let curry = Trans.goal (fun pr t -> [create_prop_decl Pgoal pr (curry t)]) let () = let () = Trans.register_transform "curry" curry Trans.register_transform "prop_curry" curry ~desc:"Currify." ~desc:"Transform@ conjunctions@ in@ implication@ premises@ into@ \ sequences@ of@ premises."
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!