def Lean.Elab.mkInhabitantFor (failedToMessage : MessageData) (xs : Array Expr) (type : Expr) : MetaM Expr

Equations

• One or more equations did not get rendered due to their size.