Mentions légales du service

Skip to content

congruence transformation

Raphaël Rieu-Helft requested to merge f_equal into master

After getting stuck on goals of the form f a1 b1 c1 = f a2 b2 c2 with a1 = a2, b1 = b2, c1 = c2, I added a transformation to handle this. This is equivalent to Coq's f_equal tactic but only handles the case where the function symbols are the same.

Edited by Raphaël Rieu-Helft

Merge request reports