def Lean.Elab.mkInhabitantFor (declName : Lake.Name) (xs : Array Lean.Expr) (type : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

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