The theorem_wanted, def_wanted, and instance_wanted commands

Use theorem_wanted name binders : T to mark a theorem the library should eventually contain without blocking compilation; def_wanted name binders : T does the same for any Sort, not just Prop. Each elaborates to a private placeholder def name binders : ProofWanted T := ⟨⟩ (resp. DefWanted T), so the wanted result is visible to downstream files and tools by type rather than by side-channel. proof_wanted is a synonym for theorem_wanted.

Inside any of these commands, ❰foo❱ references an earlier wanted declaration; for parametrised foo, write ❰foo❱ x y to apply it. When the referenced wanted's payload is a typeclass, the generated parameter is an instance binder, so Lean's instance synth can pick it up at use sites (including via Π-instance synth when chained through another wanted).

A body may be supplied with ... := body; it must reference at least one ❰…❱ (in the statement or the body). A complete proof, construction, or instance should be a theorem, def, or instance instead, and the error includes a Try this: suggestion to that effect.

There are two flavours of wanted declaration:

• Opaque holes — a bodyless def_wanted/theorem_wanted/instance_wanted (and any theorem_wanted/proof_wanted/instance_wanted, with or without a body). These elaborate to a private placeholder def foo binders : DefWanted T := ⟨⟩ (resp. ProofWanted T). A ❰foo❱ reference desugars to a fresh parameter binder of type DefWanted.Val (@foo …) (resp. .Stmt), so foo appears in the recorded type but is never inhabited.
• Transparent (derived) defs — a def_wanted with a body. This elaborates to a genuine @[reducible] def foo binders : DerivedWanted T := ⟨body⟩, and ❰foo❱ inlines it (projecting the carried value with .val), so ❰foo❱ is definitionally equal to body. This lets you build honest accessors and derived data on top of opaque holes — e.g. project a field out of a bundled wanted, with the projection actually reducing downstream — while the DerivedWanted wrapper keeps the declaration from being used directly as a value of T (only ❰…❱ accesses it).

Either way, a ❰foo❱ reference surfaces foo's own transitive leaf-hole dependencies as binders on the referencing declaration, threading them through; opaque holes stay as d_…/h_… binders, transparent intermediates are inlined away. Because the only un-filled pieces are opaque DefWanted/ProofWanted placeholders (never axiom/sorry), the whole construction is sound: a transparent def is a real definition parametrised over its hypothetical leaves.

instance_wanted name : ClassT is a variant of def_wanted whose payload must be a typeclass and whose declared name is registered file-locally, so a later wanted can use it via typeclass synth without an explicit ❰…❱ reference. Inclusion is on use (like variable [inst]): a later declaration carries the instance binder only when its statement or body actually needs it, not unconditionally. (It is always an opaque hole, even with a body.)

The ❰ and ❱ characters (U+2770, U+2771) are entered as \h< and \h> with the standard Lean input method.

structure ProofWanted (α : Sort u) : Type

Wrapper recording that a proof_wanted of statement α has been declared.

@[reducible]

def ProofWanted.Stmt {α : Sort u} : ProofWanted α → Sort u

Reducible accessor so a binder of type ProofWanted.Stmt foo reduces to foo's statement. Used by the desugaring of ❰foo❱ when foo is a proof_wanted.

Equations

• x✝.Stmt = α

structure DefWanted (α : Sort u) : Type

Wrapper recording that a def_wanted of type α has been declared.

@[reducible]

def DefWanted.Val {α : Sort u} : DefWanted α → Sort u

Reducible accessor so a binder of type DefWanted.Val foo reduces to foo's type. Used by the desugaring of ❰foo❱ when foo is a def_wanted.

Equations

• x✝.Val = α

structure DerivedWanted (α : Sort u) : Sort (max 1 u)

Wrapper carrying the body of a transparent def_wanted (one given a := body). Unlike the empty DefWanted, it stores the value, so ❰foo❱ projects it back out and downstream definitional equalities go through; but the placeholder still has type DerivedWanted T, not T, so it cannot be used directly as an inhabitant of T — the intended access is via the ❰…❱ syntax, which projects the value back out. (val is public, so direct projection is possible, but ❰…❱ is what callers should use.)

• ofVal :: (
• val : α

  The carried value. Reference the declaration via ❰…❱ rather than projecting this directly.

• )

def wantedRef : Lean.ParserDescr

Internal bracket syntax ❰foo❱ for referencing an earlier theorem_wanted or def_wanted. Only meaningful inside the statement or body of one of those commands; the term elaborator errors everywhere else.

Equations

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

def elabWantedRef : Lean.Elab.Term.TermElab

Elaborator that errors when ❰…❱ is used outside a wanted-declaration command.

Equations

• elabWantedRef x✝¹ x✝ = Lean.throwError (Lean.toMessageData "`❰…❱` may only appear inside the statement or body of `theorem_wanted`, `proof_wanted`, `def_wanted`, or `instance_wanted`")

def theorem_wanted : Lean.Parser.Parser

This proof would be a welcome contribution to the library!

The syntax of theorem_wanted declarations is just like that of theorem. Without := and a proof body it records a wanted theorem; with one it records a partial proof that still depends on other wanted lemmas. Lean checks that theorem_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), and records a private placeholder declaration of type ... → ProofWanted statement.

Modifiers (such as @[simp]) are accepted for syntactic compatibility with theorem but are currently ignored.

proof_wanted is a synonym for theorem_wanted.

Inside another theorem_wanted or def_wanted, write ❰foo❱ to reference an earlier theorem_wanted or def_wanted named foo. The bracket may appear in the statement or the body, and each distinct reference becomes a fresh parameter binder of the matching type. For parametrised foo : ∀ args, ProofWanted _, the binder type is itself Π-quantified, so ❰foo❱ x y applies the parameter to x y. ❰foo❱ only resolves names within the current file, since the placeholders are private.

A body must reference at least one ❰…❱ (in the statement or the body); otherwise the body is a complete proof and the declaration should be a theorem.

Typical usage:

-- A parameterless wanted fact:
theorem_wanted size_of_two_pushes_onto_empty :
    ((#[] : Array Nat).push 1 |>.push 2).size = 2

-- Referencing an earlier `theorem_wanted` inside a statement (here in the `Fin`
-- bound proof, which rewrites by the wanted fact):
theorem_wanted first_index_after_two_pushes :
    (⟨0, by rw [❰size_of_two_pushes_onto_empty❱]; decide⟩
      : Fin ((#[] : Array Nat).push 1 |>.push 2).size).val = 0

-- A parametrised wanted fact:
theorem_wanted size_after_two_pushes {α : Type _} (a : Array α) (x y : α) :
    ((a.push x).push y).size = a.size + 2

-- Referencing the parametrised wanted with arguments: `❰foo❱ a x y`.
theorem_wanted index_after_two_pushes {α : Type _} (a : Array α) (x y : α) :
    (⟨a.size, by rw [❰size_after_two_pushes❱ a x y]; omega⟩
      : Fin ((a.push x).push y).size).val = a.size

-- A partial proof may be supplied with `:= body`, deferring the harder step via `❰…❱`:
theorem_wanted size_after_three_pushes {α : Type _} (a : Array α) (x y z : α) :
    (((a.push x).push y).push z).size = a.size + 3 := by
  rw [Array.size_push, ❰size_after_two_pushes❱ a x y]

Equations

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

def proof_wanted : Lean.Parser.Parser

proof_wanted is a synonym for theorem_wanted; see its documentation. (It is expected to be deprecated in favour of theorem_wanted eventually.)

Equations

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

def def_wanted : Lean.Parser.Parser

This construction would be a welcome contribution to the library!

The syntax mirrors theorem_wanted but admits any Sort (not just Prop). It accepts the same ❰…❱ bracket syntax for cross-referencing earlier theorem_wanted or def_wanted declarations, including parametrised ones — ❰foo❱ x y applies foo's parameters. A body without any ❰…❱ reference is rejected with an actionable "Try this:" suggesting def.

A bodyless def_wanted records an opaque placeholder of type ... → DefWanted type (a hole). A def_wanted with a body is instead emitted as a genuine @[reducible] definition of type ... → DerivedWanted type (carrying the body), so ❰foo❱ inlines it and is definitionally equal to its body — letting you derive honest accessors and data on top of opaque holes. The DerivedWanted wrapper keeps it from being used directly as a value of type; only ❰…❱ accesses it. Either way no axiom/sorry is introduced (see the module docstring).

Modifiers (such as @[simp]) are accepted for syntactic compatibility with def but are currently ignored.

Typical usage:

def_wanted decision_procedure (n : Nat) : Decidable (Nat.Prime n)

def_wanted prime_dec_3 : Decidable (Nat.Prime 3) := ❰decision_procedure❱ 3

Equations

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

def elabTheoremWanted : Lean.Elab.Command.CommandElab

Parses the surface syntax of theorem_wanted and forwards to the shared elabWanted.

Equations

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

def elabProofWanted : Lean.Elab.Command.CommandElab

Parses the surface syntax of proof_wanted (a synonym for theorem_wanted) and forwards to the shared elabWanted.

Equations

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

def elabDefWanted : Lean.Elab.Command.CommandElab

Parses the surface syntax of def_wanted and forwards to the shared elabWanted.

Equations

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

def instance_wanted : Lean.Parser.Parser

This typeclass instance would be a welcome contribution to the library!

The syntax mirrors instance (the name is optional, auto-generated from the class head if absent) and the payload must be a typeclass. The placeholder is recorded as DefWanted (TheClass …) like def_wanted, but additionally the declared name is registered so a subsequent theorem_wanted / def_wanted / instance_wanted can use it via typeclass synth without an explicit ❰…❱ reference — matching the auto-availability of regular instance declarations.

Inclusion is on use (like variable [inst]): a later declaration carries a [d_…] binder for an earlier instance_wanted only when its statement or body actually uses it. A declaration that does not need the instance does not carry it, so unrelated instances do not accumulate as a file grows. The registration is module-scoped and order-sensitive: only instance_wanteds declared earlier in the current file are candidates. Registrations persist across section / namespace boundaries within the file and are dropped at module boundaries (the placeholder defs are private, so nothing propagates to importers).

Typical usage:

def_wanted Jacobian (C : Over (Spec (.of k))) [IsProper C.hom] : Over (Spec (.of k))

instance_wanted : GrpObj (❰Jacobian❱ C)

theorem_wanted comp_ofCurve … : … = η[❰Jacobian❱ C]
  -- automatically picks up the GrpObj instance, no haveI needed

Equations

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

def elabInstanceWanted : Lean.Elab.Command.CommandElab

Parses the surface syntax of instance_wanted, generates a name if absent, forwards to the shared elabWanted, validates the payload is a typeclass, and registers the declared name in wantedInstancesExt so subsequent wanted declarations auto-include it.

Equations

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