Informal definitions and lemmas

This file contains the necessary structures that must be imported into a file for it to contain informal definitions and lemmas.

Everything else about informal definitions and lemmas are in the Informal.Post module.

structure InformalDefinition : Type

The structure representing an informal definition.

• deps : List Lean.Name

  The names of top-level commands we expect this definition to depend on.

• tag : String

  The tag of the informal definition. This should be unique amongst informal results and todo items.

structure InformalLemma : Type

The structure representing an informal lemma.

• deps : List Lean.Name

  The names of top-level commands we expect this lemma to depend on.

• tag : String

  The tag of the informal lemma. This should be unique amongst informal results and todo items.

Syntax

Using macros for syntax rewriting works better with the language server compared to Lake.DSL.LeanLibDecl. Hovering over any definition of informal_definition or informal_lemma gives a proper type hint like any proper definition using def whereas definitions of lake_lib and lake_exe don't show docstrings and infer the type Lean.Name.

def Informal.informalDefinitionDecl : Lean.ParserDescr

A placeholder for definitions to be formalized in the future. Docstrings of informal definitions should outline its mathematical or physical content and specify useful references. Use the attribute note_attr_informal from PhysLean.Meta.Notes.Basic to mark the informal definition as a note.

Equations

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

def Informal.informalLemmaDecl : Lean.ParserDescr

A placeholder for lemmas to be formalized in the future. Docstrings of informal lemmas should outline its mathematical or physical content and specify useful references. Use the attribute note_attr_informal from PhysLean.Meta.Notes.Basic to mark the informal definition as a note.

Equations

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