Zulip Chat Archive

Stream: general

Topic: structure projections and def_lemma linter


Junyan Xu (Dec 25 2022 at 21:34):

currently blocking #18013

import tactic.lint.default

/-- -/
structure A : Prop := (x : true)

#print A.x
/- This should ideally be `lemma` rather than `@[reducible] def`:
@[reducible]
def A.x : A → true :=
λ (self : A), [A.x self]
-/

alias A.x  x
/- `A.x` itself doesn't trigger the def_lemma linter, but creating an alias triggers it. -/

#lint
/-
/- Checking 2 declarations (plus 8 automatically generated ones) in the current file with 26 linters -/

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

Junyan Xu (Dec 25 2022 at 21:38):

Another (possibly unrelated) problem is that the universe of a structure seems to default to Type (not Type*, not Sort*) even if all its fields are Props.

structure A := (x : true)
#print A
/-
structure A : Type
fields:
A.x : A → true
-/

This has caused some unintended universes in mathlib, like docs#category_theory.monoidal_preadditive and docs#category_theory.monoidal_linear. But it's easy to fix, just add : Prop.


Last updated: Dec 20 2023 at 11:08 UTC