mathlib documentation

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

This produces defs or theorems of the form:

/-- doc string -/
@[alias] theorem alias1 : <type of my_theorem> := my_theorem

/-- doc string -/
@[alias] theorem alias2 : <type of my_theorem> := my_theorem

Iff alias syntax:

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.

meta inductive tactic.alias.target  :
Type

An alias can be in one of three forms

Instances for tactic.alias.target

The name underlying an alias target

The docstring for an alias. Used by alias and by to_additive

An auxiliary attribute which is placed on definitions created by the alias command.

The core tactic which handles alias d ← al. Creates an alias al for declaration d.

meta def tactic.alias.mk_iff_mp_app (iffmp : name) :
expr(expr)tactic expr

Given a proof of Π x y z, a ↔ b, produces a proof of Π x y z, a → b or Π x y z, b → a (depending on whether iffmp is iff.mp or iff.mpr). The variable f supplies the proof, under the specified number of binders.

meta def tactic.alias.alias_iff (doc : option string) (d : declaration) (ns al : name) (is_forward : bool) :

The core tactic which handles alias d ↔ al _ or alias d ↔ _ al. ns is the current namespace, and is_forward is true if this is the forward implication (the first form).

Get the default names for left/right to be used by alias d ↔ ...

The alias command can be used to create copies of a theorem or definition with different names.

Syntax:

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

This produces defs or theorems of the form:

/-- doc string -/
@[alias] theorem alias1 : <type of my_theorem> := my_theorem

/-- doc string -/
@[alias] theorem alias2 : <type of my_theorem> := my_theorem

Iff alias syntax:

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.

The alias command can be used to create copies of a theorem or definition with different names.

Syntax:

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

This produces defs or theorems of the form:

/-- doc string -/
@[alias] theorem alias1 : <type of my_theorem> := my_theorem

/-- doc string -/
@[alias] theorem alias2 : <type of my_theorem> := my_theorem

Iff alias syntax:

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.

Given a definition, look up the definition that it is an alias of. Returns none if this defintion is not an alias.