Lean4
/-- given a `ContextInfo`, a `LocalContext` and an `Array` of `Expr`essions `es` with a `Name`,
`toFormat_propTypes` creates a `MetaM` context, and returns an array of
the pretty-printed `Format` of `e`, together with the (unchanged) name
for each `Expr`ession `e` in `es` whose type is a `Prop`.
Concretely, `toFormat_propTypes` runs `inferType` in `CommandElabM`.
This is the kind of monadic lift that `nonPropHaves` uses to decide whether the Type of a `have`
is in `Prop` or not.
The output `Format` is just so that the linter displays a better message. -/
def toFormat_propTypes (ctx : ContextInfo) (lc : LocalContext) (es : Array (Expr × Name)) :
CommandElabM (Array (Format × Name)) := do
ctx.runMetaM lc do
es.filterMapM fun (e, name) ↦ do
let typ ← inferType (← instantiateMVars e)
if typ.isProp then
return none
else
return (← ppExpr e, name)
