Docs for include suggest that it might affect def

[david-christiansen]

Description

Based on the documentation comment for include:

include eeny meeny instructs Lean to include the section variables eeny and meeny in all declarations in the remainder of the current section, differing from the default behavior of conditionally including variables based on use in the declaration header. include is usually followed by the in combinator to limit the inclusion to the subsequent declaration.

I would expect that it affected def and inductive. We should probably fix this by updating these docs.

Steps to Reproduce

Write the following code:

variable
  {α : Type u} {β : Type v}
  (f : α → β) (g : β → α)

include g

def optMap (o : Option α) : Option β :=
  match o with
  | none => none
  | some x => some (f x)

#check optMap

Expected behavior:

I would expect this signature:

optMap.{u, v} {α : Type u} {β : Type v} (f : α → β) (g : β → α) (o : Option α) : Option β

Actual behavior:
This signature:

optMap.{u, v} {α : Type u} {β : Type v} (f : α → β) (o : Option α) : Option β

Versions

"4.11.0-rc2"

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[digama0]

I would expect that it affected def and inductive. We should probably fix this by updating these docs.

I would also expect that, and think we should fix it by making it actually do that. Having variables have slightly different behavior depending on which command is being used (keeping in mind that there is a relatively large and open ended list of command keywords) seems like a difficult thing to get in users' heads.

[Kha]

Let's first fix the status quo