eta for structures

Stream: general

[Reid Barton]

Is definitional eta for structures something we are likely to get at some point?

[Gabriel Ebner]

I'd be surprised.

[Reid Barton]

In the absence of eta, another feature request would be "lazy matching" in lambdas and lets

[Reid Barton]

analogous to ~ patterns in Haskell

[Gabriel Ebner]

For everyone else, this means λ \<x,y\>, x + y gets desugared to λ p, p.1 + p.2. I don't think it is planned, but you might be able to do the desugaring yourself.

[Reid Barton]

There are some definitions in data.equiv for example which I can't use conveniently, because they match on the input equivalence before producing a constructor.

[Reid Barton]

But rewriting them with the constructor outermost becomes quite ugly.

[Reid Barton]

(not at computer, and don't remember the specific names)

[Reid Barton]

Was imagining including a ~ in the syntax for lazy patterns, not changing the current semantics.

[Reid Barton]

Though I wonder when you would ever want the "strict" version, figuratively speaking.

[Patrick Massot]

For everyone else, this means λ \<x,y\>, x + y gets desugared to λ p, p.1 + p.2. I don't think it is planned, but you might be able to do the desugaring yourself.

+1 I keep trying to type that and being disappointed.

[Mario Carneiro]

Someone recently pointed out a mathlib definition that uses case analysis like this that was causing problems, but now I can't find it. Can anyone else find it?

[Chris Hughes]

+ and * in localization.

[Mario Carneiro]

are you sure? I don't see that when I search in the chat

[Chris Hughes]

I definitely made a comment about it, but there's probably something else as well.

[Chris Hughes]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/match.20in.20defs

[Mario Carneiro]

ah, okay (I searched for "localization")

[Kenny Lau]

Should we replace those definitions with the better definitions?