## Stream: lean4

### Topic: parens on method LHS

#### Reid Barton (Jan 28 2021 at 14:26):

Is it intended that this program compiles?

class C (α : Type) where
op : α → α → α

instance : C Nat where
op (a b) := a + b    -- should be op a b := a + b


#### Sebastian Ullrich (Jan 28 2021 at 14:26):

I think so, it's no different from def op (a b) := a + b

#### Reid Barton (Jan 28 2021 at 14:27):

It can lead to bewildering error messages if one tries to write something like

inductive X
| mk : Nat → X

instance : C X where
op (X.mk a) (X.mk b) := X.mk (a + b)    -- function of 4 variables?


#### Sebastian Ullrich (Jan 28 2021 at 14:27):

That is, it's a group of binders without type

hmm, I see

#### Reid Barton (Jan 28 2021 at 14:28):

I'm not very good at predicting what Lean 4 will understand yet

#### Kevin Buzzard (Jan 28 2021 at 14:28):

I don't see! How does op (a b) even parse?

#### Reid Barton (Jan 28 2021 at 14:29):

Well this whole where ... construction is new

#### Sebastian Ullrich (Jan 28 2021 at 14:31):

Think of it as def op (a b : _), aka def op (a : _) (b : _)

#### Sebastian Ullrich (Jan 28 2021 at 14:41):

@Reid Barton I think the rule here is that op is a signature and we do not support direct pattern matching in signatures. But certainly we shouldn't accept X.mk as a binder name. If it had errored with "expected atomic identifier", do you think that would have led you to the right path?

#### Reid Barton (Jan 28 2021 at 14:41):

That should probably be an error in any case, yeah

#### Reid Barton (Jan 28 2021 at 14:41):

I didn't really expect putting a pattern there to work, but then I got confused when it sort-of worked instead

#### Mario Carneiro (Jan 28 2021 at 15:01):

Why can't patterns go there? That's how it would work in haskell

#### Mario Carneiro (Jan 28 2021 at 15:01):

how do you write an equation compiler definition in a where clause?

#### Sebastian Ullrich (Jan 28 2021 at 15:04):

It's a signature, so name binders | equations

#### Mario Carneiro (Jan 28 2021 at 15:07):

So:

inductive X
| mk : Nat → X

instance : C X where
op : X -> X -> X
| (X.mk a) (X.mk b) := X.mk (a + b)


?

#### Mario Carneiro (Jan 28 2021 at 15:07):

or are there supposed to be commas now

#### Mario Carneiro (Jan 28 2021 at 15:08):

Is the type ascription optional?

#### Sebastian Ullrich (Jan 28 2021 at 17:16):

Yes to both

instance : C X where
op
| X.mk a, X.mk b => X.mk (a + b)


Last updated: May 18 2021 at 23:14 UTC