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

@[implicit_reducible]

instance Batteries.Tactic.Alias.instInhabitedAliasInfo : Inhabited AliasInfo

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

The name underlying an alias target

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

The docstring for an alias.

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.

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

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

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

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.

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.

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).

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.