structure fields which are functions are better with `where`

Stream: lean4

[Kevin Buzzard]

structure Foo where
  bar (a b : Nat) : a = b → a = b

def x : Foo where
  bar a b h := h -- works

def y : Foo where
  bar := λ a b h => h -- works

def z : Foo := {
  -- bar a b h := h -- error `'a' is not a field of structure 'Foo'`
  bar := λ a b h => h -- works (but is longer)
}

Is this the sort of thing that people are interested in hearing? The asymmetry just struck me as odd.

[Mario Carneiro]

This could be considered as an extension of structure field syntax. I think it would be nice to support this kind of thing almost everywhere, for example in binders:

def foo (f (x : A) : A) : A
-- is equivalent to
def foo (f : A -> A) : A
def foo : (A -> A) -> A

[Kevin Buzzard]

By the way, sometimes I am forced to use the { } syntax because I am using _inst_ with.

[Mario Carneiro]

I suppose ..s notation could work with where