Lean.Elab.PreDefinition.MkInhabitant

Equations

Lean.Elab.mkInhabitantFor declName xs type = let go? := fun useOfNonempty => do let a ← Lean.Elab.mkInhabitant? type useOfNonempty match a with | some val => Lean.Internal.coeM (Lean.Meta.mkLambdaFVars xs val false true) | none => do let a ← Lean.Elab.findAssumption? xs type match a with | some x => Lean.Internal.coeM (Lean.Meta.mkLambdaFVars xs x false true) | none => do let a ← Lean.Elab.mkFnInhabitant? xs type useOfNonempty match a with | some val => pure (some val) | none => pure none; do let a ← go? false match a with | some val => pure val | none => do let a ← go? true match a with | some val => pure val | none => Lean.throwError (Lean.toMessageData "failed to compile partial definition '" ++ Lean.toMessageData declName ++ Lean.toMessageData "', failed to show that type is inhabited and non empty")