# Documentation

Mathlib.Tactic.Alias

# The alias command #

This file defines an alias command, which can be used to create copies of a theorem or definition with different names.

Syntax:

/-- doc string -/
alias my_theorem ← alias1 alias2 ...
← alias1 alias2 ...


This produces defs or theorems of the form:

/-- doc string -/
theorem alias1 :  := my_theorem

/-- doc string -/
theorem alias2 :  := my_theorem


Iff alias syntax:

alias A_iff_B ↔ B_of_A A_of_B
alias A_iff_B ↔ ..
↔ B_of_A A_of_B
alias A_iff_B ↔ ..
↔ ..


This gets an existing biconditional theorem A_iff_B and produces the one-way implications B_of_A and A_of_B (with no change in implicit arguments). A blank _ can be used to avoid generating one direction. The .. notation attempts to generate the 'of'-names automatically when the input theorem has the form A_iff_B or A_iff_B_left etc.

Adds some copies of a theorem or definition.

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

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

Adds one-way implication declarations, inferring names for them.

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

Like ++, except that if the right argument starts with _root_ the namespace will be ignored.

appendNamespace a.b c.d = a.b.c.d
appendNamespace a.b _root_.c.d = c.d


TODO: Move this declaration to a more central location.

Equations
• plain:
• forward:
• backwards:

An alias can be in one of three forms

Instances For

The name underlying an alias target

Equations
• = match x with | => n | => n | => n

The docstring for an alias.

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

Elaborates an alias ←← command.

Equations
• One or more equations did not get rendered due to their size.
def Tactic.Alias.mkIffMpApp (mp : Bool) (ty : Lean.Expr) (prf : 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 Tactic.Alias.aliasIff (doc : Option (Lean.TSyntax Lean.Parser.Command.docComment)) (ci : Lean.ConstantInfo) (ref : Lean.Syntax) (al : Lean.Name) (isForward : Bool) :

Given a constant representing an iff decl, adds a decl for one of the implication directions.

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

Elaborates an alias ↔↔ command.

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

Elaborates an alias ↔ ..↔ ..` command.

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