Write a tactic `rewrite_assoc` that performs rewriting mod associativity of composition.

b-mehta / topos

Topos theory in lean

56 stars 2 forks source link

Open EdAyers opened 4 years ago

EdAyers commented 4 years ago

Seems like a net win and it doesn't have to be a full-blown monster tactic like tidy.

Vtec234 commented 4 years ago

b-mehta commented 4 years ago

Oh nice! This looks exactly like what we wanted