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).
Instances For
Instances For
Instances For
Instances For
declModifiers
is the collection of modifiers on a declaration:
- a doc comment
/-! ... -/
- a list of attributes
@[attr1, attr2]
- a visibility specifier,
private
orprotected
noncomputable
unsafe
partial
ornonrec
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.
Instances For
declId
matches foo
or foo.{u,v}
: an identifier possibly followed by a list of universe names
Instances For
declSig
matches the signature of a declaration with required type: a list of binders and then : type
Instances For
optDeclSig
matches the signature of a declaration with optional type: a list of binders and then possibly : type
Instances For
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 amatch
where
and then a sequence offield := value
initializers, shorthand for a structure constructor
Instances For
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.
Instances For
This is an auxiliary command for generation constructor injectivity theorems for
inductive types defined at Prelude.lean
.
It is meant for bootstrapping purposes only.
Instances For
No-op parser used as syntax kind for attaching remaining whitespace to at the end of the input.
Instances For
declModifiers
is the collection of modifiers on a declaration:
- a doc comment
/-! ... -/
- a list of attributes
@[attr1, attr2]
- a visibility specifier,
private
orprotected
noncomputable
unsafe
partial
ornonrec
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.
Instances For
declModifiers
is the collection of modifiers on a declaration:
- a doc comment
/-! ... -/
- a list of attributes
@[attr1, attr2]
- a visibility specifier,
private
orprotected
noncomputable
unsafe
partial
ornonrec
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.
Instances For
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
.
Instances For
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
.