CoqIde: показать, что делает простая тактика
Используя CoqIde, есть ли способ просмотреть шаги simpl взят? Я нахожу, что не понимаю, как он достиг своего результата довольно часто.
Пример:
rev (rev (n :: l')) = n :: l'
-- apply simpl.
rev (rev l' ++ [n]) = n :: l'