field projections inside begin..end blocks

Stream: general

[Bernd Losert]

I have this code:

class foo :=
(bar : nat) (baz : nat -> nat)

open foo

def silly (x : foo) : foo := {
  bar := begin
    let xbar := x.bar,
    let xbaz := x.baz 0,
  end,
  baz := nat.succ
}

Unfortunately, lean does not like it:

error: invalid field notation, function 'foo.baz' does not have explicit argument with type (foo ...)

It's weird that x.bar works, but x.baz doesn't. How do I work around this?

[Bernd Losert]

If I change from class to structure, the error goes away.

[Kyle Miller]

It's because (strangely) it takes the foo implicitly as an instance argument:

#check @foo.baz
/-
foo.baz : Π [self : foo], ℕ → ℕ
-/

[Reid Barton]

It's annoying to try to use instances as values. In this case you should imitate topological_space and only define your thing to be a class after the fact, like here:
https://github.com/leanprover-community/mathlib/blob/a8c086fe2de3c950a50932c953aa9a1d44543391/src/topology/basic.lean#L65
This way the field projections will be generated with more useful types.

[Bernd Losert]

Let me try.

[Bernd Losert]

Yep, seems to work. That's one interesting "gotcha". I'll have to keep it in mind.