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.

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.

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.