Control for lemma command

The lemma command exists in Mathlib, but not in Std.

This file enforces the convention by introducing a code-action to replace lemma by theorem.

opaque Batteries.Tactic.Lemma.lang.lemmaCmd : Lean.Option Bool

Enables the use of lemma as a synonym for theorem

def Batteries.Tactic.Lemma.checkLangLemmaCmd (o : Lean.Options) : Bool

Check whether lang.lemmaCmd option is enabled

Equations

• Batteries.Tactic.Lemma.checkLangLemmaCmd o = Lean.KVMap.get o `lang.lemmaCmd Batteries.Tactic.Lemma.lang.lemmaCmd.defValue

def Batteries.Tactic.Lemma.lemmaCmd : Lean.ParserDescr

lemma is not supported, please use theorem instead

Equations

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

def Batteries.Tactic.Lemma.elabLemma : Lean.Elab.Command.CommandElab

Elaborator for the lemma command, if the option lang.lemmaCmd is false the command emits a warning and code action instructing the user to use theorem instead.

Equations

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