source
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.

Instances For

source
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.

Instances For