Confusing placeholder behaviour

Stream: new members

[Laurance Lau]

Apologies, for I do not know where it is appropriate to put this. The code I wish to discuss (part of Combinatorics/SimpleGraph/Basic) is very brief and is reproduced below:

structure SimpleGraph (V : Type u) where
  /-- The adjacency relation of a simple graph. -/
  Adj : V → V → Prop
  symm : Symmetric Adj := by aesop_graph
  loopless : Irreflexive Adj := by aesop_graph

def emptyGraph (V : Type u) : SimpleGraph V where Adj _ _ := False

The definition of emptyGraph uses placeholders to say that the adjacency relation is always False. However, the way this is presented in the documentation, which is the presentation I first saw, is

emptyGraph V = { Adj := fun (x x : V) => False, symm := ⋯, loopless := ⋯ }

This was confusing to me because a SimpleGraph is loopless by definition, so of course fun (x x : V) => False, where I thought the xs are identical, should always be the case. This is also how it also appears in the tactic state whenever I do rw [emptyGraph] in the middle of a proof, yet the xs do behave as different variables.

I am very inexperienced and am wondering whether my confusion could have been avoided.

[Matt Diamond]

It's unfortunate that the docs generated the code fun (x x : V) => False... I can see how that could be confusing for a newcomer. The truth is that the two xs are not identical, they're just identically named.

[Matt Diamond]

Normally a function with duplicated argument names is bad because it means that previously listed arguments are inaccessible... if you try to reference them, you'll end up referencing the most recently declared one. However, this doesn't matter when the function is always returning False, since there's no need to reference any of the arguments.

[Kyle Miller]

This fun (x x : V) => False issue is on my radar (#lean4 > Prettyprinter prints fun x x => ... @ 💬 ). I think it ought to be fixed, though I don't have a specific plan to fix it yet.

[Kyle Miller]

In this case, we probably should print each x as _ since the variable isn't being used, and the actual name isn't x internally (it's supposed to be some inaccessible name).