Documentation

Init.Conv

source
def Lean.Parser.Tactic.Conv.conv.quot:
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.Conv.convSeq1Indented:
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.Conv.convSeqBracketed:
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.Conv.convSeq:
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.Conv.conv:
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.Conv.lhs:
Lean.ParserDescr
Equations
source
def Lean.Parser.Tactic.Conv.rhs:
Lean.ParserDescr
Equations
source
def Lean.Parser.Tactic.Conv.whnf:
Lean.ParserDescr
Equations
source
def Lean.Parser.Tactic.Conv.zeta:
Lean.ParserDescr

Expand let-declarations and let-variables.

Equations
source
def Lean.Parser.Tactic.Conv.reduce:
Lean.ParserDescr

Put term in normal form, this tactic is ment for debugging purposes only

Equations
source
def Lean.Parser.Tactic.Conv.congr:
Lean.ParserDescr
Equations
source
def Lean.Parser.Tactic.Conv.arg:
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.Conv.ext:
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.Conv.change:
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.Conv.delta:
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.Conv.unfold:
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.Conv.pattern:
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.Conv.rewrite:
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.Conv.simp:
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.Conv.simpMatch:
Lean.ParserDescr
Equations
source
def Lean.Parser.Tactic.Conv.nestedTacticCore:
Lean.ParserDescr

Execute the given tactic block without converting conv goal into a regular goal

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.Conv.nestedTactic:
Lean.ParserDescr

Focus, convert the conv goal ⊢ lhs into a regular goal ⊢ lhs = rhs, and then execute the given tactic block.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.Conv.nestedConv:
Lean.ParserDescr
Equations
source
def Lean.Parser.Tactic.Conv.paren:
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.Conv.convConvSeq:
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.Conv.«conv·._»:
Lean.ParserDescr

· conv focuses on the main conv goal and tries to solve it using s

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.Conv.convRw__:
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.Conv.convErw_:
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.Conv.convArgs:
Lean.ParserDescr
Equations
source
def Lean.Parser.Tactic.Conv.convLeft:
Lean.ParserDescr
Equations
source
def Lean.Parser.Tactic.Conv.convRight:
Lean.ParserDescr
Equations
source
def Lean.Parser.Tactic.Conv.convIntro__:
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.Conv.enterArg:
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.Conv.«convEnter[__]»:
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.Conv.convSkip:
Lean.ParserDescr
Equations
source
def Lean.Parser.Tactic.Conv.convDone:
Lean.ParserDescr
Equations
source
def Lean.Parser.Tactic.Conv.convTrace_state:
Lean.ParserDescr
Equations
source
def Lean.Parser.Tactic.Conv.convApply_:
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.Conv.first:
Lean.ParserDescr

first | conv | ... runs each conv until one succeeds, or else fails.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.Conv.convRepeat_:
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.