The alias command

The alias command is used to create synonyms. The plain command can create a synonym of any declaration. There is also a version to create synonyms for the forward and reverse implications of an iff theorem.

inductive Batteries.Tactic.Alias.AliasInfo : Type

An alias can be in one of three forms

• plain (n : Lean.Name) : AliasInfo

  Plain alias

• forward (n : Lean.Name) : AliasInfo

  Forward direction of an iff alias

• reverse (n : Lean.Name) : AliasInfo

  Reverse direction of an iff alias

instance Batteries.Tactic.Alias.instInhabitedAliasInfo : Inhabited AliasInfo

Equations

• Batteries.Tactic.Alias.instInhabitedAliasInfo = { default := Batteries.Tactic.Alias.AliasInfo.plain default }

def Batteries.Tactic.Alias.AliasInfo.name : AliasInfo → Lean.Name

The name underlying an alias target

Equations

• (Batteries.Tactic.Alias.AliasInfo.plain n).name = n
• (Batteries.Tactic.Alias.AliasInfo.forward n).name = n
• (Batteries.Tactic.Alias.AliasInfo.reverse n).name = n

def Batteries.Tactic.Alias.AliasInfo.toString : AliasInfo → String

The docstring for an alias.

Equations

• (Batteries.Tactic.Alias.AliasInfo.plain n).toString = toString "**Alias** of `" ++ toString n ++ toString "`."
• (Batteries.Tactic.Alias.AliasInfo.forward n).toString = toString "**Alias** of the forward direction of `" ++ toString n ++ toString "`."
• (Batteries.Tactic.Alias.AliasInfo.reverse n).toString = toString "**Alias** of the reverse direction of `" ++ toString n ++ toString "`."

opaque Batteries.Tactic.Alias.aliasExt : Lean.SimpleScopedEnvExtension (Lean.Name × AliasInfo) (Lean.NameMap AliasInfo)

Environment extension for registering aliases

def Batteries.Tactic.Alias.getAliasInfo {m : Type → Type} [Monad m] [Lean.MonadEnv m] (name : Lean.Name) : m (Option AliasInfo)

Get the alias information for a name

Equations

• Batteries.Tactic.Alias.getAliasInfo name = do let __do_lift ← Lean.getEnv pure ((Lean.ScopedEnvExtension.getState Batteries.Tactic.Alias.aliasExt __do_lift).find? name)

def Batteries.Tactic.Alias.setAliasInfo {m : Type → Type} [Lean.MonadEnv m] (info : AliasInfo) (declName : Lean.Name) : m Unit

Set the alias info for a new declaration

Equations

• Batteries.Tactic.Alias.setAliasInfo info declName = Lean.modifyEnv fun (x : Lean.Environment) => Lean.ScopedEnvExtension.addEntry Batteries.Tactic.Alias.aliasExt x (declName, info)

def Batteries.Tactic.Alias.setDeprecatedTarget (target : Lean.Name) (arr : Array Lean.Elab.Attribute) : Array Lean.Elab.Attribute × Bool

Updates the deprecated declaration to point to target if no target is provided.

Equations

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

def Batteries.Tactic.Alias.alias : Lean.ParserDescr

The command alias name := target creates a synonym of target with the given name.

The command alias ⟨fwd, rev⟩ := target creates synonyms for the forward and reverse directions of an iff theorem. Use _ if only one direction is required.

These commands accept all modifiers and attributes that def and theorem do.

Equations

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

def Batteries.Tactic.Alias.mkIffMpApp (mp : Bool) (ty prf : Lean.Expr) : Lean.MetaM Lean.Expr

Given a possibly forall-quantified iff expression prf, produce a value for one of the implication directions (determined by mp).

Equations

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

def Batteries.Tactic.Alias.aliasLR : Lean.ParserDescr

The command alias name := target creates a synonym of target with the given name.

The command alias ⟨fwd, rev⟩ := target creates synonyms for the forward and reverse directions of an iff theorem. Use _ if only one direction is required.

These commands accept all modifiers and attributes that def and theorem do.

Equations

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