Commit 835fdffb authored by Felipe Cerqueira's avatar Felipe Cerqueira

Add tactic to simplify sum of constant

parent d985591a
......@@ -11,7 +11,7 @@
(** Symbols starting with [vlib__] are internal. *)
Require Import ssreflect ssrbool ssrnat eqtype.
Require Import ssreflect ssrbool ssrnat eqtype bigop.
Open Scope bool_scope.
Open Scope list_scope.
......@@ -449,4 +449,12 @@ Ltac feed H :=
Ltac feed_n n H := match constr:n with
| O => idtac
| (S ?m) => feed H ; [| feed_n m H]
end.
\ No newline at end of file
end.
(* ************************************************************************** *)
(** * New tactics for ssreflect *)
(* ************************************************************************** *)
Ltac simpl_sum_const :=
rewrite ?big_const_nat ?big_const_ord ?big_const_seq iter_addn ?muln1 ?mul1n ?mul0n
?muln0 ?addn0 ?add0n.
\ No newline at end of file
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment