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 Std.Tactic.Alias.AliasInfo : Type

• plain: Lean.Name → Std.Tactic.Alias.AliasInfo

  Plain alias

• forward: Lean.Name → Std.Tactic.Alias.AliasInfo

  Forward direction of an iff alias

• reverse: Lean.Name → Std.Tactic.Alias.AliasInfo

  Reverse direction of an iff alias

An alias can be in one of three forms

instance Std.Tactic.Alias.instInhabitedAliasInfo : Inhabited Std.Tactic.Alias.AliasInfo

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

The name underlying an alias target

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

The docstring for an alias.

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

Environment extension for registering aliases

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

Get the alias information for a name

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

Set the alias info for a new declaration

def Std.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 Std.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 Std.Tactic.Alias.mkIffMpApp (mp : Bool) (ty : Lean.Expr) (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 Std.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.