Topic: equality by components
Reid Barton (Feb 27 2018 at 15:54):
If my goal is of the form
⟨x, y⟩ = ⟨x', y'⟩, is there a tactic that will replace it with two new goals
x = x' and
y = y'?
Reid Barton (Feb 27 2018 at 15:56):
congr did it.
Reid Barton (Feb 27 2018 at 16:21):
I'm also wondering how I could do this when the left and/or right hand side is not already a constructor application, and I want to eta expand first. (But in my actual case the right hand side was just a variable, and I could use
Mario Carneiro (Feb 27 2018 at 17:54):
Lean doesn't have definitional eta for products fyi
Last updated: May 11 2021 at 13:22 UTC