Documentation

Lean.Elab.PreDefinition.MkInhabitant

source
def Lean.Elab.mkInhabitantFor (declName : Lean.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.