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_reducible]

instance Batteries.Tactic.Alias.instInhabitedAliasInfo : Inhabited AliasInfo

Equations

• Batteries.Tactic.Alias.instInhabitedAliasInfo = { default := Batteries.Tactic.Alias.instInhabitedAliasInfo.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 "`."

def Batteries.Tactic.Alias.addAliasDocstring (declName : Lean.Name) (info : AliasInfo) : Lean.CoreM Unit

Add a docstring to the alias declName if it doesn't already have one. This needs to run after elaboration of attributes, because e.g. inherit_doc could a add docstring. This is also used in to_additive/to_dual.

Equations

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

opaque Batteries.Tactic.Alias.aliasExt : Lean.MapDeclarationExtension 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 (Batteries.Tactic.Alias.aliasExt.find? __do_lift name)

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

Get the old alias information for a name.

@[deprecated "use `getAliasInfo?` or `getOldAliasInfo?` for the original behavior" (since := "2026-04-11")]

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 = Batteries.Tactic.Alias.getOldAliasInfo? name

partial def Batteries.Tactic.Alias.getAliasPath {m : Type → Type} [Monad m] [Lean.MonadEnv m] (name : Lean.Name) : m (List Bool × Lean.Name)

Returns the path of aliases starting at a given name.

The return value is a pair (mps, name) where name is the final non-aliased name in the alias chain and mps is a list of Bool indicating the sequence of forward (true) and reverse (false) aliases along the chain.

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) => Batteries.Tactic.Alias.aliasExt.insert 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.isReducibilityAttr (attr : Lean.Name) : Bool

Whether attr is one of the attributes that set the reducibility status of a definition.

Equations

• Batteries.Tactic.Alias.isReducibilityAttr `reducible = true
• Batteries.Tactic.Alias.isReducibilityAttr `semireducible = true
• Batteries.Tactic.Alias.isReducibilityAttr `irreducible = true
• Batteries.Tactic.Alias.isReducibilityAttr `implicit_reducible = true
• Batteries.Tactic.Alias.isReducibilityAttr `instance_reducible = true
• Batteries.Tactic.Alias.isReducibilityAttr attr = false

def Batteries.Tactic.Alias.declNamespace? (declName : Lean.Name) : Option Lean.Name

The namespace that def opens while elaborating a declaration named declName: Foo.Bar for Foo.Bar.baz, and none for atomic names and names starting with _root_.

Equations

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

def Batteries.Tactic.Alias.realizeAliasTarget (aliasName : Lean.Name) (target : Lean.Ident) : Lean.Elab.TermElabM Lean.Name

Resolves the target of an alias named aliasName. If target cannot be resolved in the ambient scope, it is resolved again with the namespace of aliasName open, as def would do. The ambient scope is tried first so that existing aliases keep resolving to the same constants.

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.

An alias of a definition has the same reducibility status as its target, so an alias of an abbrev is reducible. A reducibility attribute on the alias, such as @[irreducible], sets its status instead.

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.

An alias of a definition has the same reducibility status as its target, so an alias of an abbrev is reducible. A reducibility attribute on the alias, such as @[irreducible], sets its status instead.

Equations

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