mathlib3 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
@[protected, instance]
meta def tactic.alias.target.has_reflect  :
has_reflect tactic.alias.target
source
meta inductive tactic.alias.target  :
Type

An alias can be in one of three forms

Instances for tactic.alias.target
source
meta def tactic.alias.target.to_name  :
tactic.alias.target → name

The name underlying an alias target

source
meta def tactic.alias.target.to_string  :
tactic.alias.target → string

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

source
meta def tactic.alias.alias_attr  :
user_attribute unit tactic.alias.target

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

source
meta def tactic.alias.alias_direct (doc : option string) (d : declaration) (al : name) :
tactic unit

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

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

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

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

source
meta def tactic.alias.make_left_right  :
name → tactic (name × name)

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

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
def tactic_doc.command.alias  :
tactic_doc_entry

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_alias_target (n : name) :
tactic (option tactic.alias.target)

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