hygiene frontend bug?

Stream: lean4

[Arthur Paulino]

I'm not sure if this is a bug in core or in the infoview, but I found this:

example {P Q : Prop} (hp : P → Q) (p : P) : True := by
-- P Q : Prop
-- hp ​: P →
-- p : P
-- ⊢ True
  have hp := hp p
-- P Q : Prop
--  : P → Q               should be `hp† : P → Q` ?
-- p : P
-- hp : Q
-- ⊢ True
  trivial

It's no biggie, but I just wanted to bring it to awareness. LMK if I should open an issue (and in which repo)

[Henrik Böving]

No this is an intentional feature I saw in one of the recent nightlies, shadowed names are not shown on purpose anymore since it confuses the user less.

Now you being used to them are of course more confused than before :P

[Arthur Paulino]

I'm using leanprover/lean4:nightly-2022-04-06 and the lean4 extension v0.0.70

[Henrik Böving]

This nightly did it https://github.com/leanprover/lean4-nightly/releases/tag/nightly-2022-04-03

[Arthur Paulino]

I'm not sure this is the best way to approach this tho. My current context is full of variables and then I see this:

⋯
xs : NEList String
 : NEList.noDup ns = true →
  consume p' ns (NEList.cons e es) = (some (NEList.cons x xs), p) → NEList.noDup (NEList.cons x xs) = true
⋯

My first reaction was to think it was related to xs because of the indentation. Maybe it should show at least a dagger (†) before the :

[Mario Carneiro]

I would suggest _ for this purpose

[Arthur Paulino]

Either would be nice, just to keep the pattern bla : ble

[Leonardo de Moura]

@Arthur Paulino Please keep in mind that you are using Lean 4 as we change its behavior. This kind of confusion is inevitable as developers change the behavior of something you are used to. Please give it a try and see how you feel about it in a few days.

[Arthur Paulino]

It's just a piece of feedback. The example shown in the changelog might not look so pretty if the order is arbitrary like this:

β : Type u_1
 : k < key
b : BinTree β
k : Nat
v : β
left : Tree β
key : Nat
 : BST left
value : β
 : ForallTree (fun k v => k < key) left
right : Tree β
 : BST right
ihl : BST left → Tree.find? (Tree.insert left k v) k = some v
 : ForallTree (fun k v => key < k) right
ihr : BST right → Tree.find? (Tree.insert right k v) k = some v
⊢ BST left

[Mario Carneiro]

I still think that _ makes the most sense here, since this is already what we use in binders to indicate that the value is in scope but the name is not accessible

[Mario Carneiro]

it makes copy-paste editing to do a manual extract_goal easier too (although you still have to add the parens, since whitespace sensitivity isn't a thing for binder groups AFAIK)

[Leonardo de Moura]

Mario Carneiro said:

I still think that _ makes the most sense here, since this is already what we use in binders to indicate that the value is in scope but the name is not accessible

Thanks for the feedback. We will keep observing how other users react to this change.

[Jad Ghalayini]

My 2 cents is that I actually prefer the new look quite a bit haha