Old-style Prop-valued structures

Stream: general

[Oliver Nash]

I want to set up some structures like this:

import data.nat.basic

set_option old_structure_cmd true

structure foo (n : ℕ) : Prop := (zero_lt : 0 < n)

structure bar (n : ℕ) extends foo n : Prop := (even : n % 2 = 0)

#print bar.to_foo -- We see it's a `def` rather than a `lemma`

[Oliver Nash]

The two important points are:

• Using set_option old_structure_cmd true
• These are Prop-valued structures

[Oliver Nash]

However (thanks to the linter) I discovered that the above code makes the projection bar.to_foo a def rather than a lemma.

[Oliver Nash]

I'm not sure what to do about this. Does it matter?

[Anne Baanen]

That's weird, but I expect no bad effects beyond linter warning and a little bit of useless code generation. The more dangerous direction would be a lemma that should be a def.