Documentation

Lean.Parser.Command

Syntax quotation for terms.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    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).

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

        /-! <text> -/ defines a module docstring that can be displayed by documentation generation tools. The string is associated with the corresponding position in the file. It can be used multiple times in the same file.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Equations
                      • One or more equations did not get rendered due to their size.
                      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.

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

                          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.
                          Instances For

                            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.
                            Instances For

                              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.
                              Instances For

                                Right-hand side of a := in a declaration, a term.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        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
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    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 constructors. 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 α. See Inductive types for more information.

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

                                                                                                    A section/end pair delimits the scope of variable, include, open, set_option, and localcommands. Sections can be nested.section <id>provides a label to the section that has to appear with the matchingend. In either case, the end` can be omitted, in which case the section is closed at the end of the file.

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

                                                                                                      namespace <id> opens a section with label <id> that influences naming and name resolution inside the section:

                                                                                                      • Declarations names are prefixed: def seventeen : ℕ := 17 inside a namespace Nat is given the full name Nat.seventeen.
                                                                                                      • Names introduced by export declarations are also prefixed by the identifier.
                                                                                                      • All names starting with <id>. become available in the namespace without the prefix. These names are preferred over names introduced by outer namespaces or open.
                                                                                                      • Within a namespace, declarations can be protected, which excludes them from the effects of opening the namespace.

                                                                                                      As with section, namespaces can be nested and the scope of a namespace is terminated by a corresponding end <id> or the end of the file.

                                                                                                      namespace also acts like section in delimiting the scope of variable, open, and other scoped commands.

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

                                                                                                        end closes a section or namespace scope. If the scope is named <id>, it has to be closed with end <id>. The end command is optional at the end of a file.

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

                                                                                                          Declares one or more typed variables, or modifies whether already-declared variables are implicit.

                                                                                                          Introduces variables that can be used in definitions within the same namespace or section block. When a definition mentions a variable, Lean will add it as an argument of the definition. This is useful in particular when writing many definitions that have parameters in common (see below for an example).

                                                                                                          Variable declarations have the same flexibility as regular function parameters. In particular they can be [explicit, implicit][binder docs], or [instance implicit][tpil classes] (in which case they can be anonymous). This can be changed, for instance one can turn explicit variable x into an implicit one with variable {x}. Note that currently, you should avoid changing how variables are bound and declare new variables at the same time; see [issue 2789] for more on this topic.

                                                                                                          In theorem bodies (i.e. proofs), variables are not included based on usage in order to ensure that changes to the proof cannot change the statement of the overall theorem. Instead, variables are only available to the proof if they have been mentioned in the theorem header or in an include command or are instance implicit and depend only on such variables.

                                                                                                          See Variables and Sections from Theorem Proving in Lean for a more detailed discussion.

                                                                                                          (Variables and Sections on Theorem Proving in Lean) [tpil classes]: https://lean-lang.org/theorem_proving_in_lean4/type_classes.html (Type classes on Theorem Proving in Lean) [binder docs]: https://leanprover-community.github.io/mathlib4_docs/Lean/Expr.html#Lean.BinderInfo (Documentation for the BinderInfo type) [issue 2789]: https://github.com/leanprover/lean4/issues/2789 (Issue 2789 on github)

                                                                                                          Examples #

                                                                                                          section
                                                                                                            variable
                                                                                                              {α : Type u}      -- implicit
                                                                                                              (a : α)           -- explicit
                                                                                                              [instBEq : BEq α] -- instance implicit, named
                                                                                                              [Hashable α]      -- instance implicit, anonymous
                                                                                                          
                                                                                                            def isEqual (b : α) : Bool :=
                                                                                                              a == b
                                                                                                          
                                                                                                            #check isEqual
                                                                                                            -- isEqual.{u} {α : Type u} (a : α) [instBEq : BEq α] (b : α) : Bool
                                                                                                          
                                                                                                            variable
                                                                                                              {a} -- `a` is implicit now
                                                                                                          
                                                                                                            def eqComm {b : α} := a == b ↔ b == a
                                                                                                          
                                                                                                            #check eqComm
                                                                                                            -- eqComm.{u} {α : Type u} {a : α} [instBEq : BEq α] {b : α} : Prop
                                                                                                          end
                                                                                                          

                                                                                                          The following shows a typical use of variable to factor out definition arguments:

                                                                                                          variable (Src : Type)
                                                                                                          
                                                                                                          structure Logger where
                                                                                                            trace : List (Src × String)
                                                                                                          #check Logger
                                                                                                          -- Logger (Src : Type) : Type
                                                                                                          
                                                                                                          namespace Logger
                                                                                                            -- switch `Src : Type` to be implicit until the `end Logger`
                                                                                                            variable {Src}
                                                                                                          
                                                                                                            def empty : Logger Src where
                                                                                                              trace := []
                                                                                                            #check empty
                                                                                                            -- Logger.empty {Src : Type} : Logger Src
                                                                                                          
                                                                                                            variable (log : Logger Src)
                                                                                                          
                                                                                                            def len :=
                                                                                                              log.trace.length
                                                                                                            #check len
                                                                                                            -- Logger.len {Src : Type} (log : Logger Src) : Nat
                                                                                                          
                                                                                                            variable (src : Src) [BEq Src]
                                                                                                          
                                                                                                            -- at this point all of `log`, `src`, `Src` and the `BEq` instance can all become arguments
                                                                                                          
                                                                                                            def filterSrc :=
                                                                                                              log.trace.filterMap
                                                                                                                fun (src', str') => if src' == src then some str' else none
                                                                                                            #check filterSrc
                                                                                                            -- Logger.filterSrc {Src : Type} (log : Logger Src) (src : Src) [inst✝ : BEq Src] : List String
                                                                                                          
                                                                                                            def lenSrc :=
                                                                                                              log.filterSrc src |>.length
                                                                                                            #check lenSrc
                                                                                                            -- Logger.lenSrc {Src : Type} (log : Logger Src) (src : Src) [inst✝ : BEq Src] : Nat
                                                                                                          end Logger
                                                                                                          

                                                                                                          The following example demonstrates availability of variables in proofs:

                                                                                                          variable
                                                                                                            {α : Type}    -- available in the proof as indirectly mentioned through `a`
                                                                                                            [ToString α]  -- available in the proof as `α` is included
                                                                                                            (a : α)       -- available in the proof as mentioned in the header
                                                                                                            {β : Type}    -- not available in the proof
                                                                                                            [ToString β]  -- not available in the proof
                                                                                                          
                                                                                                          theorem ex : a = a := rfl
                                                                                                          

                                                                                                          After elaboration of the proof, the following warning will be generated to highlight the unused hypothesis:

                                                                                                          included section variable '[ToString α]' is not used in 'ex', consider excluding it
                                                                                                          

                                                                                                          In such cases, the offending variable declaration should be moved down or into a section so that only theorems that do depend on it follow it until the end of the section.

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

                                                                                                            Declares one or more universe variables.

                                                                                                            universe u v

                                                                                                            Prop, Type, Type u and Sort u are types that classify other types, also known as universes. In Type u and Sort u, the variable u stands for the universe's level, and a universe at level u can only classify universes that are at levels lower than u. For more details on type universes, please refer to the relevant chapter of Theorem Proving in Lean.

                                                                                                            Just as type arguments allow polymorphic definitions to be used at many different types, universe parameters, represented by universe variables, allow a definition to be used at any required level. While Lean mostly handles universe levels automatically, declaring them explicitly can provide more control when writing signatures. The universe keyword allows the declared universe variables to be used in a collection of definitions, and Lean will ensure that these definitions use them consistently.

                                                                                                            /- Explicit type-universe parameter. -/
                                                                                                            def id₁.{u} (α : Type u) (a : α) := a
                                                                                                            
                                                                                                            /- Implicit type-universe parameter, equivalent to `id₁`.
                                                                                                              Requires option `autoImplicit true`, which is the default. -/
                                                                                                            def id₂ (α : Type u) (a : α) := a
                                                                                                            
                                                                                                            /- Explicit standalone universe variable declaration, equivalent to `id₁` and `id₂`. -/
                                                                                                            universe u
                                                                                                            def id₃ (α : Type u) (a : α) := a
                                                                                                            

                                                                                                            On a more technical note, using a universe variable only in the right-hand side of a definition causes an error if the universe has not been declared previously.

                                                                                                            def L₁.{u} := List (Type u)
                                                                                                            
                                                                                                            -- def L₂ := List (Type u) -- error: `unknown universe level 'u'`
                                                                                                            
                                                                                                            universe u
                                                                                                            def L₃ := List (Type u)
                                                                                                            

                                                                                                            Examples #

                                                                                                            universe u v w
                                                                                                            
                                                                                                            structure Pair (α : Type u) (β : Type v) : Type (max u v) where
                                                                                                              a : α
                                                                                                              b : β
                                                                                                            
                                                                                                            #check Pair.{v, w}
                                                                                                            -- Pair : Type v → Type w → Type (max v w)
                                                                                                            
                                                                                                            Equations
                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                            Instances For
                                                                                                              Equations
                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                              Instances For
                                                                                                                Equations
                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                Instances For
                                                                                                                  Equations
                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                  Instances For
                                                                                                                    Equations
                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                    Instances For
                                                                                                                      Equations
                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                      Instances For
                                                                                                                        Equations
                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                        Instances For
                                                                                                                          Equations
                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                          Instances For
                                                                                                                            Equations
                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                            Instances For
                                                                                                                              Equations
                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                              Instances For

                                                                                                                                Displays all available tactic tags, with documentation.

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

                                                                                                                                      set_option <id> <value> sets the option <id> to <value>. Depending on the type of the option, the value can be true, false, a string, or a numeral. Options are used to configure behavior of Lean as well as user-defined extensions. The setting is active until the end of the current section or namespace or the end of the file. Auto-completion is available for <id> to list available options.

                                                                                                                                      set_option <id> <value> in <command> sets the option for just a single command:

                                                                                                                                      set_option pp.all true in
                                                                                                                                      #check 1 + 1
                                                                                                                                      

                                                                                                                                      Similarly, set_option <id> <value> in can also be used inside terms and tactics to set an option only in a single term or tactic.

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

                                                                                                                                            Adds names from other namespaces to the current namespace.

                                                                                                                                            The command export Some.Namespace (name₁ name₂) makes name₁ and name₂:

                                                                                                                                            • visible in the current namespace without prefix Some.Namespace, like open, and
                                                                                                                                            • visible from outside the current namespace N as N.name₁ and N.name₂.

                                                                                                                                            Examples #

                                                                                                                                            namespace Morning.Sky
                                                                                                                                              def star := "venus"
                                                                                                                                            end Morning.Sky
                                                                                                                                            
                                                                                                                                            namespace Evening.Sky
                                                                                                                                              export Morning.Sky (star)
                                                                                                                                              -- `star` is now in scope
                                                                                                                                              #check star
                                                                                                                                            end Evening.Sky
                                                                                                                                            
                                                                                                                                            -- `star` is visible in `Evening.Sky`
                                                                                                                                            #check Evening.Sky.star
                                                                                                                                            
                                                                                                                                            Equations
                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                            Instances For
                                                                                                                                              Equations
                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                              Instances For
                                                                                                                                                Equations
                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                Instances For
                                                                                                                                                  Equations
                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                  Instances For
                                                                                                                                                    Equations
                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                    Instances For
                                                                                                                                                      Equations
                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                      Instances For
                                                                                                                                                        Equations
                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                        Instances For
                                                                                                                                                          Equations
                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                          Instances For

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

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

                                                                                                                                                              Makes names from other namespaces visible without writing the namespace prefix.

                                                                                                                                                              Names that are made available with open are visible within the current section or namespace block. This makes referring to (type) definitions and theorems easier, but note that it can also make [scoped instances], notations, and attributes from a different namespace available.

                                                                                                                                                              The open command can be used in a few different ways:

                                                                                                                                                              • open Some.Namespace.Path1 Some.Namespace.Path2 makes all non-protected names in Some.Namespace.Path1 and Some.Namespace.Path2 available without the prefix, so that Some.Namespace.Path1.x and Some.Namespace.Path2.y can be referred to by writing only x and y.

                                                                                                                                                              • open Some.Namespace.Path hiding def1 def2 opens all non-protected names in Some.Namespace.Path except def1 and def2.

                                                                                                                                                              • open Some.Namespace.Path (def1 def2) only makes Some.Namespace.Path.def1 and Some.Namespace.Path.def2 available without the full prefix, so Some.Namespace.Path.def3 would be unaffected.

                                                                                                                                                                This works even if def1 and def2 are protected.

                                                                                                                                                              • open Some.Namespace.Path renaming def1 → def1', def2 → def2' same as open Some.Namespace.Path (def1 def2) but def1/def2's names are changed to def1'/def2'.

                                                                                                                                                                This works even if def1 and def2 are protected.

                                                                                                                                                              • open scoped Some.Namespace.Path1 Some.Namespace.Path2 only opens [scoped instances], notations, and attributes from Namespace1 and Namespace2; it does not make any other name available.

                                                                                                                                                              • open <any of the open shapes above> in makes the names open-ed visible only in the next command or expression.

                                                                                                                                                              Examples #

                                                                                                                                                              /-- SKI combinators https://en.wikipedia.org/wiki/SKI_combinator_calculus -/
                                                                                                                                                              namespace Combinator.Calculus
                                                                                                                                                                def I (a : α) : α := a
                                                                                                                                                                def K (a : α) : β → α := fun _ => a
                                                                                                                                                                def S (x : α → β → γ) (y : α → β) (z : α) : γ := x z (y z)
                                                                                                                                                              end Combinator.Calculus
                                                                                                                                                              
                                                                                                                                                              section
                                                                                                                                                                -- open everything under `Combinator.Calculus`, *i.e.* `I`, `K` and `S`,
                                                                                                                                                                -- until the section ends
                                                                                                                                                                open Combinator.Calculus
                                                                                                                                                              
                                                                                                                                                                theorem SKx_eq_K : S K x = I := rfl
                                                                                                                                                              end
                                                                                                                                                              
                                                                                                                                                              -- open everything under `Combinator.Calculus` only for the next command (the next `theorem`, here)
                                                                                                                                                              open Combinator.Calculus in
                                                                                                                                                              theorem SKx_eq_K' : S K x = I := rfl
                                                                                                                                                              
                                                                                                                                                              section
                                                                                                                                                                -- open only `S` and `K` under `Combinator.Calculus`
                                                                                                                                                                open Combinator.Calculus (S K)
                                                                                                                                                              
                                                                                                                                                                theorem SKxy_eq_y : S K x y = y := rfl
                                                                                                                                                              
                                                                                                                                                                -- `I` is not in scope, we have to use its full path
                                                                                                                                                                theorem SKxy_eq_Iy : S K x y = Combinator.Calculus.I y := rfl
                                                                                                                                                              end
                                                                                                                                                              
                                                                                                                                                              section
                                                                                                                                                                open Combinator.Calculus
                                                                                                                                                                  renaming
                                                                                                                                                                    I → identity,
                                                                                                                                                                    K → konstant
                                                                                                                                                              
                                                                                                                                                                #check identity
                                                                                                                                                                #check konstant
                                                                                                                                                              end
                                                                                                                                                              
                                                                                                                                                              section
                                                                                                                                                                open Combinator.Calculus
                                                                                                                                                                  hiding S
                                                                                                                                                              
                                                                                                                                                                #check I
                                                                                                                                                                #check K
                                                                                                                                                              end
                                                                                                                                                              
                                                                                                                                                              section
                                                                                                                                                                namespace Demo
                                                                                                                                                                  inductive MyType
                                                                                                                                                                  | val
                                                                                                                                                              
                                                                                                                                                                  namespace N1
                                                                                                                                                                    scoped infix:68 " ≋ " => BEq.beq
                                                                                                                                                              
                                                                                                                                                                    scoped instance : BEq MyType where
                                                                                                                                                                      beq _ _ := true
                                                                                                                                                              
                                                                                                                                                                    def Alias := MyType
                                                                                                                                                                  end N1
                                                                                                                                                                end Demo
                                                                                                                                                              
                                                                                                                                                                -- bring `≋` and the instance in scope, but not `Alias`
                                                                                                                                                                open scoped Demo.N1
                                                                                                                                                              
                                                                                                                                                                #check Demo.MyType.val == Demo.MyType.val
                                                                                                                                                                #check Demo.MyType.val ≋ Demo.MyType.val
                                                                                                                                                                -- #check Alias -- unknown identifier 'Alias'
                                                                                                                                                              end
                                                                                                                                                              
                                                                                                                                                              Equations
                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                              Instances For
                                                                                                                                                                Equations
                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                Instances For
                                                                                                                                                                  Equations
                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                  Instances For
                                                                                                                                                                    Equations
                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                    Instances For
                                                                                                                                                                      Equations
                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                      Instances For

                                                                                                                                                                        Adds a docstring to an existing declaration, replacing any existing docstring. The provided docstring should be written as a docstring for the add_decl_doc command, as in

                                                                                                                                                                        /-- My new docstring -/
                                                                                                                                                                        add_decl_doc oldDeclaration
                                                                                                                                                                        

                                                                                                                                                                        This is useful for auto-generated declarations for which there is no place to write a docstring in the source code.

                                                                                                                                                                        Parent projections in structures are an example of this:

                                                                                                                                                                        structure Triple (α β γ : Type) extends Prod α β where
                                                                                                                                                                          thrd : γ
                                                                                                                                                                        
                                                                                                                                                                        /-- Extracts the first two projections of a triple. -/
                                                                                                                                                                        add_decl_doc Triple.toProd
                                                                                                                                                                        

                                                                                                                                                                        Documentation can only be added to declarations in the same module.

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

                                                                                                                                                                          Register a tactic tag, saving its user-facing name and docstring.

                                                                                                                                                                          Tactic tags can be used by documentation generation tools to classify related tactics.

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

                                                                                                                                                                            Add more documentation as an extension of the documentation for a given tactic.

                                                                                                                                                                            The extended documentation is placed in the command's docstring. It is shown as part of a bulleted list, so it should be brief.

                                                                                                                                                                            Equations
                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                            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.

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

                                                                                                                                                                                include eeny meeny instructs Lean to include the section variables eeny and meeny in all theorems in the remainder of the current section, differing from the default behavior of conditionally including variables based on use in the theorem header. Other commands are not affected. include is usually followed by in theorem ... to limit the inclusion to the subsequent declaration.

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

                                                                                                                                                                                  omit instructs Lean to not include a variable previously included. Apart from variable names, it can also refer to typeclass instance variables by type using the syntax omit [TypeOfInst], in which case all instance variables that unify with the given type are omitted. omit should usually only be used in conjunction with in in order to keep the section structure simple.

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

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

                                                                                                                                                                                    Equations
                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      @[reducible, inline]

                                                                                                                                                                                      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.

                                                                                                                                                                                      Equations
                                                                                                                                                                                      Instances For
                                                                                                                                                                                        @[reducible, inline]

                                                                                                                                                                                        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.

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

                                                                                                                                                                                          Equations
                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                          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.

                                                                                                                                                                                            Equations
                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                            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.

                                                                                                                                                                                              Equations
                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                              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.

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