Using the CoqIde, is there a way to view the steps simpl has taken? I find I do not understand how it achieved its result quite often.
Example:
rev (rev (n :: l')) = n :: l'
-- apply simpl.
rev (rev l' ++ [n]) = n :: l'
Asked
Active
Viewed 78 times
0
MaxWillmott
- 2,170
- 2
- 23
- 34
-
1This question seems to be a duplicate of this one -- https://stackoverflow.com/questions/54047766/how-does-one-inspect-what-more-complicated-tactics-do-in-coq-step-by-step – Anton Trunov Jan 12 '19 at 12:54
-
Possible duplicate of [How does one inspect what more complicated tactics do in Coq step-by-step?](https://stackoverflow.com/questions/54047766/how-does-one-inspect-what-more-complicated-tactics-do-in-coq-step-by-step) – user138737 Feb 28 '19 at 19:38