alias accidental def

Stream: general

[Yaël Dillies]

When used on a structure field, alias creates defs even though they should be lemma:

import tactic.alias
import tactic.lint

structure foo (α : Type*) :=
(bar : ∀ a b : α, a = b)

alias foo.bar ← baz

#lint

/- Checking 2 declarations (plus 13 automatically generated ones) in the current file with 23 linters -/

/- The `def_lemma` linter reports: -/
/- INCORRECT DEF/LEMMA: -/
#check @baz /- is a def, should be a lemma/theorem -/

I assume a simple fix would be to make alias check whether the field is Prop-valued or not. I have no idea how to do that, though.

[Eric Wieser]

cmd#alias should be the start of the breadcrumb...

[Eric Wieser]

Aw man, no linkifier

[Yakov Pechersky]

(deleted)

[Alex J. Best]

foo.bar is a def though, so alias is just copying that. Do you want it to check if the type is Prop and automatically make it a lemma, or rather have some syntax like alias lemma blah \l foo ?

[Eric Wieser]

Perhaps we need to fix lean core to generate prop projections as lemmas instead?

[Yaël Dillies]

Oh yeah this sounds like the correct fix. Is it how it works behind the scenes? A structure declaration gets turned into many defs?