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.

source
meta def tactic.alias.alias_attr  :
(user_attribute unit)
source
meta def tactic.alias.alias_direct (d : declaration) (doc : string) (al : name) :
tactic unit
source
meta def tactic.alias.mk_iff_mp_app (iffmp : name) :
expr → (ℕ → expr) → tactic expr
source
meta def tactic.alias.alias_iff (d : declaration) (doc : string) (al iffmp : name) :
tactic unit
source
meta def tactic.alias.make_left_right  :
name → tactic (name × name)
source
meta def tactic.alias.alias_cmd (meta_info : interactive.decl_meta_info) (_x : interactive.parse (lean.parser.tk "alias")) :
lean.parser unit

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.

source
meta def tactic.alias.get_lambda_body  :
expr → expr
source
meta def tactic.alias.get_alias_target (n : name) :
tactic (option name)