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

Syntax quotation for terms.

Equations

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

def Lean.Parser.Term.precheckedQuot : Lean.Parser.Parser

Equations

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

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.

def Lean.Parser.Command.terminationHintMany (p : Lean.Parser.Parser) : Lean.Parser.Parser

Equations

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

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.

def Lean.Parser.Command.terminationHint (p : Lean.Parser.Parser) : Lean.Parser.Parser

Equations

• Lean.Parser.Command.terminationHint p = HOrElse.hOrElse (Lean.Parser.Command.terminationHintMany p) fun x => Lean.Parser.Command.terminationHint1 p

def Lean.Parser.Command.terminationByCore : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.decreasingBy : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.terminationByElement : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.terminationBy : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.terminationSuffix : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.moduleDoc : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.namedPrio : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.optNamedPrio : Lean.Parser.Parser

Equations

• Lean.Parser.Command.optNamedPrio = Lean.Parser.optional Lean.Parser.Command.namedPrio

def Lean.Parser.Command.private : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.protected : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.visibility : Lean.Parser.Parser

Equations

• Lean.Parser.Command.visibility = HOrElse.hOrElse Lean.Parser.Command.private fun x => Lean.Parser.Command.protected

def Lean.Parser.Command.noncomputable : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.unsafe : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.partial : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.nonrec : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.declModifiers (inline : Bool) : Lean.Parser.Parser

declModifiers is the collection of modifiers on a declaration:

• a doc comment /-! ... -/
• a list of attributes @[attr1, attr2]
• a visibility specifier, private or protected
• noncomputable
• unsafe
• partial or nonrec

All modifiers are optional, and have to come in the listed order.

nestedDeclModifiers is the same as declModifiers, but attributes are printed on the same line as the declaration. It is used for declarations nested inside other syntax, such as inductive constructors, structure projections, and let rec / where definitions.

Equations

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

def Lean.Parser.Command.declId : Lean.Parser.Parser

declId matches foo or foo.{u,v}: an identifier possibly followed by a list of universe names

Equations

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

def Lean.Parser.Command.declSig : Lean.Parser.Parser

declSig matches the signature of a declaration with required type: a list of binders and then : type

Equations

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

def Lean.Parser.Command.optDeclSig : Lean.Parser.Parser

optDeclSig matches the signature of a declaration with optional type: a list of binders and then possibly : type

Equations

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

def Lean.Parser.Command.declValSimple : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.declValEqns : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.whereStructField : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.whereStructInst : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.declVal : Lean.Parser.Parser

declVal matches the right-hand side of a declaration, one of:

• := expr (a "simple declaration")
• a sequence of | pat => expr (a declaration by equations), shorthand for a match
• where and then a sequence of field := value initializers, shorthand for a structure constructor

Equations

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

def Lean.Parser.Command.abbrev : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.optDefDeriving : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.def : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.theorem : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.opaque : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.instance : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.axiom : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.example : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.ctor : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.derivingClasses : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.optDeriving : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.computedField : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.computedFields : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.inductive : Lean.Parser.Parser

In Lean, every concrete type other than the universes and every type constructor other than dependent arrows is an instance of a general family of type constructions known as inductive types. It is remarkable that it is possible to construct a substantial edifice of mathematics based on nothing more than the type universes, dependent arrow types, and inductive types; everything else follows from those. Intuitively, an inductive type is built up from a specified list of constructor. For example, List α is the list of elements of type α, and is defined as follows:

inductive List (α : Type u) where
| nil
| cons (head : α) (tail : List α)

A list of elements of type α is either the empty list, nil, or an element head : α followed by a list tail : List α. For more information about inductive types.

Equations

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

def Lean.Parser.Command.classInductive : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.structExplicitBinder : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.structImplicitBinder : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.structInstBinder : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.structSimpleBinder : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.structFields : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.structCtor : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.structureTk : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.classTk : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.extends : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.structure : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.declaration : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.deriving : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.noncomputableSection : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.section : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.namespace : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.end : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.variable : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.universe : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.check : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.check_failure : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.reduce : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.eval : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.synth : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.exit : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.print : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.printAxioms : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.init_quot : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.optionValue : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.set_option : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.eraseAttr : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.attribute : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.export : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.import : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.openHiding : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.openRenamingItem : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.openRenaming : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.openOnly : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.openSimple : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.openScoped : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.openDecl : Lean.Parser.Parser

openDecl is the body of an open declaration (see open)

Equations

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

def Lean.Parser.Command.open : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.mutual : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.initializeKeyword : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.initialize : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.in : Lean.Parser.TrailingParser

Equations

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

def Lean.Parser.Command.addDocString : Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.genInjectiveTheorems : Lean.Parser.Parser

This is an auxiliary command for generation constructor injectivity theorems for inductive types defined at Prelude.lean. It is meant for bootstrapping purposes only.

Equations

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

def Lean.Parser.Command.eoi : Lean.Parser.Parser

No-op parser used as syntax kind for attaching remaining whitespace to at the end of the input.

Equations

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

@[inline, reducible]

abbrev Lean.Parser.Command.declModifiersF : Lean.Parser.Parser

declModifiers is the collection of modifiers on a declaration:

• a doc comment /-! ... -/
• a list of attributes @[attr1, attr2]
• a visibility specifier, private or protected
• noncomputable
• unsafe
• partial or nonrec

All modifiers are optional, and have to come in the listed order.

nestedDeclModifiers is the same as declModifiers, but attributes are printed on the same line as the declaration. It is used for declarations nested inside other syntax, such as inductive constructors, structure projections, and let rec / where definitions.

Equations

• Lean.Parser.Command.declModifiersF = Lean.Parser.Command.declModifiers false

@[inline, reducible]

abbrev Lean.Parser.Command.declModifiersT : Lean.Parser.Parser

declModifiers is the collection of modifiers on a declaration:

• a doc comment /-! ... -/
• a list of attributes @[attr1, attr2]
• a visibility specifier, private or protected
• noncomputable
• unsafe
• partial or nonrec

All modifiers are optional, and have to come in the listed order.

nestedDeclModifiers is the same as declModifiers, but attributes are printed on the same line as the declaration. It is used for declarations nested inside other syntax, such as inductive constructors, structure projections, and let rec / where definitions.

Equations

• Lean.Parser.Command.declModifiersT = Lean.Parser.Command.declModifiers true

def Lean.Parser.Term.open : Lean.Parser.Parser

open Foo in e is like open Foo but scoped to a single term. It makes the given namespaces available in the term e.

Equations

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

def Lean.Parser.Term.set_option : Lean.Parser.Parser

set_option opt val in e is like set_option opt val but scoped to a single term. It sets the option opt to the value val in the term e.

Equations

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

def Lean.Parser.Tactic.open : Lean.Parser.Parser

open Foo in tacs (the tactic) acts like open Foo at command level, but it opens a namespace only within the tactics tacs.

Equations

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

def Lean.Parser.Tactic.set_option : Lean.Parser.Parser

set_option opt val in tacs (the tactic) acts like set_option opt val at the command level, but it sets the option only within the tactics tacs.

Equations

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