Documentation

Batteries.Util.ProofWanted

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

    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