Documentation

Lean.Parser.Command

Syntax quotation for terms.

Instances For

    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

      declModifiers is the collection of modifiers on a declaration:

      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 a match
              • where and then a sequence of field := 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

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

                  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
                        @[inline, reducible]

                        declModifiers is the collection of modifiers on a declaration:

                        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
                          @[inline, reducible]

                          declModifiers is the collection of modifiers on a declaration:

                          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

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

                            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

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

                                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.

                                  Instances For