Zulip Chat Archive

Stream: new members

Topic: variable + explicit binders


Julian Berman (Jun 17 2021 at 11:35):

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 (Jun 17 2021 at 11:42):

include is the keyword you're looking for, IIRC

Julian Berman (Jun 17 2021 at 11:51):

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

Horatiu Cheval (Jun 17 2021 at 12:02):

Does Lean4 remove include?

Julian Berman (Jun 17 2021 at 12:36):

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


Last updated: Dec 20 2023 at 11:08 UTC