Coq-Equations icon indicating copy to clipboard operation
Coq-Equations copied to clipboard

Published 20 hours ago • verified publisher icon mattam82

Feature Request: simp equations tactic

Open yforster opened this issue 4 years ago • 0 comments

Currently, when I want to simplify a goal containing f1 and f2, both defined using Equations, I have to type simp f1 f2.

It would be great if there would be a simp equations tactic, simplifying all occurrences of functions defined using Equations in a goal.

yforster avatar Oct 19 '20 08:10 yforster