Documentation

Mathlib.Util.WhatsNew

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

whatsnew 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)
Instances For
    def Mathlib.WhatsNew.whatsNew (old new : Lean.Environment) :
    Lean.CoreM Lean.MessageData
    Instances For

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

      Instances For