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

Syntax quotation for terms.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.

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.

@[inline, reducible]

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

@[inline, reducible]

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

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.

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.

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.

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.