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

#whats_new in
theorem foo : 42 = 6 * 7 := rfl

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

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.

def Mathlib.WhatsNew.«command#whats_newIn__» : Lean.ParserDescr

#whats_new in executes the following 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.

def Mathlib.WhatsNew.oldStx : Lean.ParserDescr

#whats_new in executes the following 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.