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.

ink

def Tactic.Alias.alias : Lean.ParserDescr

Adds some copies of a theorem or definition.

Equations

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

ink

def Tactic.Alias.aliasLR : Lean.ParserDescr

Adds one-way implication declarations.

Equations

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

ink

def Tactic.Alias.aliasLRDots : Lean.ParserDescr

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

Equations

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

ink

def Tactic.Alias.appendNamespace (ns : Lean.Name) : Lean.Name → Lean.Name

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

• Tactic.Alias.appendNamespace ns (Lean.Name.str Lean.Name.anonymous s) = if s = "_root_" then Lean.Name.anonymous else Lean.Name.mkStr ns s
• Tactic.Alias.appendNamespace ns (Lean.Name.str p s) = Lean.Name.mkStr (Tactic.Alias.appendNamespace ns p) s
• Tactic.Alias.appendNamespace ns (Lean.Name.num p n) = Lean.Name.mkNum (Tactic.Alias.appendNamespace ns p) n
• Tactic.Alias.appendNamespace ns Lean.Name.anonymous = ns

ink

inductive Tactic.Alias.Target : Type

• plain: Lean.Name → Tactic.Alias.Target
• forward: Lean.Name → Tactic.Alias.Target
• backwards: Lean.Name → Tactic.Alias.Target

An alias can be in one of three forms

ink

def Tactic.Alias.Target.toName : Tactic.Alias.Target → Lean.Name

The name underlying an alias target

Equations

• Tactic.Alias.Target.toName x = match x with | Tactic.Alias.Target.plain n => n | Tactic.Alias.Target.forward n => n | Tactic.Alias.Target.backwards n => n

ink

def Tactic.Alias.Target.toString : Tactic.Alias.Target → String

The docstring for an alias.

Equations

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

ink

def Tactic.Alias.elabAlias : Lean.Elab.Command.CommandElab

Elaborates an alias ←← command.

Equations

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

ink

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

ink

def Tactic.Alias.aliasIff (doc : Option (Lean.TSyntax `Lean.Parser.Command.docComment)) (ci : Lean.ConstantInfo) (ref : Lean.Syntax) (al : Lean.Name) (isForward : Bool) : Lean.Elab.TermElabM Unit

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.

ink

def Tactic.Alias.elabAliasLR : Lean.Elab.Command.CommandElab

Elaborates an alias ↔↔ command.

Equations

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

ink

def Tactic.Alias.elabAliasLRDots : Lean.Elab.Command.CommandElab

Elaborates an alias ↔ ..↔ .. command.

Equations

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