Documentation

Lean.Parser.Command

source
def Lean.Parser.Term.quot:
Lean.Parser.Parser

Syntax quotation for terms and (lists of) commands. We prefer terms, so ambiguous quotations like `($x $y) will be parsed as an application, not two commands. Use `($x:command $y:command) instead. Multiple command will be put in a `null node, but a single command will not (so that you can directly match against a quotation in a command kind's elaborator).

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.precheckedQuot:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.quot:
Lean.Parser.Parser

Syntax quotation for (sequences of) commands. The identical syntax for term quotations takes priority, so ambiguous quotations like `($x $y) will be parsed as an application, not two commands. Use `($x:command $y:command) instead. Multiple commands will be put in a `null node, but a single command will not (so that you can directly match against a quotation in a command kind's elaborator).

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.terminationHintMany (p : Lean.Parser.Parser) :
Lean.Parser.Parser

A mutual block may be broken in different cliques, we identify them using an ident (an element of the clique) We provide two kinds of hints to the termination checker: 1- A wellfounded relation (p is termParser) 2- A tactic for proving the recursive applications are "decreasing" (p is tacticSeq)

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.terminationHint1 (p : Lean.Parser.Parser) :
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.terminationHint (p : Lean.Parser.Parser) :
Lean.Parser.Parser
Equations
source
def Lean.Parser.Command.terminationByCore:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.decreasingBy:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.terminationByElement:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.terminationBy:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.terminationSuffix:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.moduleDoc:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.namedPrio:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.optNamedPrio:
Lean.Parser.Parser
Equations
source
def Lean.Parser.Command.private:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.protected:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.visibility:
Lean.Parser.Parser
Equations
source
def Lean.Parser.Command.noncomputable:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.unsafe:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.partial:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.nonrec:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.declModifiers (inline : Bool) :
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.declId:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.declSig:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.optDeclSig:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.declValSimple:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.declValEqns:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.whereStructField:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.whereStructInst:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.declVal:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.abbrev:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.optDefDeriving:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.def:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.theorem:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.opaque:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.instance:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.axiom:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.example:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.ctor:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.derivingClasses:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.optDeriving:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.inductive:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.classInductive:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.structExplicitBinder:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.structImplicitBinder:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.structInstBinder:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.structSimpleBinder:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.structFields:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.structCtor:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.structureTk:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.classTk:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.extends:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.structure:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.declaration:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.deriving:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.noncomputableSection:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.section:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.namespace:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.end:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.variable:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.universe:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.check:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.check_failure:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.reduce:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.eval:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.synth:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.exit:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.print:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.printAxioms:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.resolve_name:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.init_quot:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.optionValue:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.set_option:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.eraseAttr:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.attribute:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.export:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.openHiding:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.openRenamingItem:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.openRenaming:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.openOnly:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.openSimple:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.openScoped:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.openDecl:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.open:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.mutual:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.initialize:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.builtin_initialize:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.in:
Lean.Parser.TrailingParser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.genInjectiveTheorems:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
@[inline]
abbrev Lean.Parser.Command.declModifiersF:
Lean.Parser.Parser
Equations
source
@[inline]
abbrev Lean.Parser.Command.declModifiersT:
Lean.Parser.Parser
Equations
source
def Lean.Parser.Term.open:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.set_option:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.open:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.set_option:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.