Semiformal results

Semiformal results sit in between informal and formal results. There type or proposition is defined, by the proof or definition is not.

## Note

The code here is modified from the Util.ProofWanted module of the Batteries library. Released under the Apache 2.0 license, copyright 2023 Lean FRO, authored by David Thrane Christiansen.

structure WantedInfo : Type

The information from a TODO ... command.

• content : String

  The content of the note.

• name : Lean.Name

  Name of result.

• fileName : Lean.Name

  The file name where the note came from.

• line : Nat

  The line from where the note came from.

• tag : String

  The tag of the TODO item

opaque wantedExtension : Lean.SimplePersistentEnvExtension WantedInfo (Array WantedInfo)

The environment extension for semiformal results.

def semiformal_result : Lean.Parser.Parser

A semiformal result is either a

• definition in which the type is given but not the definition.
• proof in which the proposition is given but not the proof. Semiformal results cannot be used in further code. They are essentially forgot about after made.

With minor modification they act in a similar way to proof_wanted, however they appear in PhysLean's TODO list and must be tagged accordingly. They must also always have a doc-string.

Equations

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

def elabLemmaWanted : Lean.Elab.Command.CommandElab

The elaborator for semiformal results.

Equations

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