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

An alias can be in one of three forms

• 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

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

Equations

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

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

The name underlying an alias target

Equations

• Std.Tactic.Alias.AliasInfo.name x = match x with | Std.Tactic.Alias.AliasInfo.plain n => n | Std.Tactic.Alias.AliasInfo.forward n => n | Std.Tactic.Alias.AliasInfo.reverse n => n

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

The docstring for an alias.

Equations

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

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

Equations

• Std.Tactic.Alias.getAliasInfo name = do let __do_lift ← Lean.getEnv pure (Lean.NameMap.find? (Lean.ScopedEnvExtension.getState Std.Tactic.Alias.aliasExt __do_lift) 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

Equations

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

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.

Equations

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

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.

Equations

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

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

Equations

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

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.

Equations

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