Lean4
/-- returns the `have` syntax whose corresponding hypothesis does not have Type `Prop` and
also a `Format`ted version of the corresponding Type. -/
partial def nonPropHaves : InfoTree → CommandElabM (Array (Syntax × Format)) :=
InfoTree.foldInfoM (init := #[]) fun ctx info args =>
return
args ++
(← do
let .ofTacticInfo i := info |
return #[]
let stx := i.stx
let .original .. := stx.getHeadInfo |
return #[]
unless isHave? stx do
return #[]
let mctx := i.mctxAfter
let mvdecls :=
i.goalsAfter.filterMap
(mctx.decls.find? ·)
-- We extract the `MetavarDecl` with largest index after a `have`, since this one
-- holds information about the metavariable where `have` introduces the new hypothesis,
-- and determine the relevant `LocalContext`.
let lc := mvdecls.toArray.getMax? (·.index < ·.index) |>.getD default |>.lctx
let oldMvdecls := i.goalsBefore.filterMap (mctx.decls.find? ·)
let oldFVars :=
(oldMvdecls.map (·.lctx.decls.toList.reduceOption)).flatten.map
(·.fvarId)
-- `newDecls` are the local declarations whose `FVarID` did not exist before the `have`.
-- Effectively they are the declarations that we want to test for being in `Prop` or not.
let newDecls :=
lc.decls.toList.reduceOption.filter
(!oldFVars.contains ·.fvarId)
-- Now, we get the `MetaM` state up and running to find the types of each entry of `newDecls`.
-- For each entry which is a `Type`, we print a warning on `have`.
let fmts ← toFormat_propTypes ctx lc (newDecls.map (fun e ↦ (e.type, e.userName))).toArray
return fmts.map fun (fmt, na) ↦ (stx, f! "{na } : {fmt}"))
