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

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.

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

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.