Documentation

Lean.Elab.PreDefinition.MkInhabitant

source
def Lean.Elab.mkInhabitantFor (failedToMessage : MessageData) (xs : Array Expr) (type : Expr) :
MetaM Expr
Equations
    Instances For