Lean4
/-- Linter that checks whether a structure should be in Prop.
-/
@[env_linter]
def structureInType : Linter
where
noErrorsFound := "no structures that should be in Prop found."
errorsFound := "FOUND STRUCTURES THAT SHOULD BE IN PROP."
test
declName := do
unless isStructure (← getEnv) declName do
return none
let isProp ←
forallTelescopeReducing (← inferType (← mkConstWithLevelParams declName)) fun _ ty ↦ return ty == .sort .zero
if isProp then
return none
let projs := (getStructureInfo? (← getEnv) declName).get!.fieldNames
if projs.isEmpty then
return none
let allProofs ←
projs.allM
(do
isProof <| ← mkConstWithLevelParams <| declName ++ ·)
unless allProofs do
return none
return m!"all fields are propositional but the structure isn't."
