variable + explicit binders

Stream: new members

[Julian Berman]

If I have variable (x : y) and then make a def that doesn't use x in its body, x doesn't become part of the def's type signature. Can I force it to be so anyways (to make projective notation work anyhow)?

I.e.:

  structure Foo where
    x := 12

  namespace Foo

  variable (foo : Foo)

  def bar := 37
  def baz := foo.x

  end Foo

  variable (quux : Foo)

I #check Foo.bar     ■ Foo.bar : Nat
I #check Foo.baz     ■ Foo.baz : Foo → Nat
I #check quux.baz     ■ Foo.baz quux : Nat
E #check quux.bar     ■ invalid field notation, function 'Foo.bar' does not have argument with type (Foo ...) that can be used, it must be explicit or implicit with an unique name

where foo.bar got treated differently than foo.baz. Obviously I can repeat the variable as a binder in the definition which is what I'm doing at the minute, but anything else I should know?

[Ruben Van de Velde]

include is the keyword you're looking for, IIRC

[Julian Berman]

Aha, thanks! That does seem to do it on Lean 3 at least.

[Horatiu Cheval]

Does Lean4 remove include?

[Julian Berman]

Unless I'm missing it I think so. Might just not be implemented yet though