parens on method LHS

Stream: lean4

[Reid Barton]

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]

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

[Reid Barton]

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]

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

[Reid Barton]

hmm, I see

[Reid Barton]

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

[Kevin Buzzard]

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

[Reid Barton]

Well this whole where ... construction is new

[Sebastian Ullrich]

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

[Sebastian Ullrich]

@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]

That should probably be an error in any case, yeah

[Reid Barton]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Sebastian Ullrich]

It's a signature, so name binders | equations

[Mario Carneiro]

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]

or are there supposed to be commas now

[Mario Carneiro]

Is the type ascription optional?

[Sebastian Ullrich]

Yes to both

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