Def Lean.Expr.isSorryAx

Modification history

2026-02-19 16:06

Mathlib/Lean/Expr/Basic.lean

feat: make the `unusedInstancesInType` linters fire when instances are not used outside of proofs in the type (#32440) …

Added Lean.Expr.isSorryAx View on Github →