(*CSC: che si guadagni nulla in fatto di efficienza. *)
let replace =
ProofEngineReduction.replace
- ~equality:(ProofEngineReduction.syntactic_equality)
+ ~equality:
+ (ProofEngineReduction.syntactic_equality ~alpha_equivalence:false)
~what:term' ~with_what:term
in
let ty' = replace ty in
let elim_type term = apply_tactic (Ring.elim_type_tac ~term)
let ring () = apply_tactic Ring.ring_tac
let fourier () = apply_tactic FourierR.fourier_tac
-
+let rewrite_simpl term = apply_tactic (FourierR.rewrite_simpl_tac ~term)