def proof_wanted : Lean.Parser.Parser

This proof would be a welcome contribution to the library!

The syntax of proof_wanted declarations is just like that of theorem, but without := or the proof. Lean checks that proof_wanted declarations are well-formed (e.g. it ensures that all the mentioned names are in scope, and that the theorem statement is a valid proposition), but they are discarded afterwards. This means that they cannot be used as axioms.

Typical usage:

@[simp] proof_wanted empty_find? [BEq α] [Hashable α] {a : α} :
    (∅ : HashMap α β).find? a = none

Equations

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

def elabProofWanted : Lean.Elab.Command.CommandElab

Elaborate a proof_wanted declaration. The declaration is translated to an axiom during elaboration, but it's then removed from the environment.

Equations

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