Defines a command wrapper that prints the changes the command makes to the environment.

    whatsnew in
    theorem foo : 42 = 6 * 7 := rfl

source
def Mathlib.WhatsNew.diffExtension (old new : Lean.Environment) (ext : Lean.PersistentEnvExtension Lean.EnvExtensionEntry Lean.EnvExtensionEntry Lean.EnvExtensionState) :
Lean.CoreM (Option Lean.MessageData)
Equations

- Mathlib.WhatsNew.diffExtension old new ext = Mathlib.WhatsNew.diffExtension.unsafe_impl_5 old new ext

Instances For

source
def Mathlib.WhatsNew.whatsNew (old new : Lean.Environment) :
Lean.CoreM Lean.MessageData
Equations

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

Instances For

source
def Mathlib.WhatsNew.commandWhatsnewIn__ :
Lean.ParserDescr

`whatsnew in $command` executes the command and then prints the declarations that were added to the environment.

Equations

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

Instances For