Documentation

Init.NotationExtra

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
        Instances For
          Equations
          Instances For
            Equations
            Instances For
              Equations
              Instances For
                def Lean.expandExplicitBinders (combinatorDeclName : Lake.Name) (explicitBinders : Lean.Syntax) (body : Lean.Syntax) :
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def Lean.expandBrackedBinders (combinatorDeclName : Lake.Name) (bracketedExplicitBinders : Lean.Syntax) (body : Lean.Syntax) :
                  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

                                            Step-wise reasoning over transitive relations.

                                            calc
                                              a = b := pab
                                              b = c := pbc
                                              ...
                                              y = z := pyz
                                            

                                            proves a = z from the given step-wise proofs. = can be replaced with any relation implementing the typeclass Trans. Instead of repeating the right- hand sides, subsequent left-hand sides can be replaced with _.

                                            calc
                                              a = b := pab
                                              _ = c := pbc
                                              ...
                                              _ = z := pyz
                                            

                                            It is also possible to write the first relation as <lhs>\n _ = <rhs> := <proof>. This is useful for aligning relation symbols, especially on longer: identifiers:

                                            calc abc
                                              _ = bce := pabce
                                              _ = cef := pbcef
                                              ...
                                              _ = xyz := pwxyz
                                            

                                            calc works as a term, as a tactic or as a conv tactic.

                                            See Theorem Proving in Lean 4 for more information.

                                            Equations
                                            Instances For

                                              Step-wise reasoning over transitive relations.

                                              calc
                                                a = b := pab
                                                b = c := pbc
                                                ...
                                                y = z := pyz
                                              

                                              proves a = z from the given step-wise proofs. = can be replaced with any relation implementing the typeclass Trans. Instead of repeating the right- hand sides, subsequent left-hand sides can be replaced with _.

                                              calc
                                                a = b := pab
                                                _ = c := pbc
                                                ...
                                                _ = z := pyz
                                              

                                              It is also possible to write the first relation as <lhs>\n _ = <rhs> := <proof>. This is useful for aligning relation symbols, especially on longer: identifiers:

                                              calc abc
                                                _ = bce := pabce
                                                _ = cef := pbcef
                                                ...
                                                _ = xyz := pwxyz
                                              

                                              calc works as a term, as a tactic or as a conv tactic.

                                              See Theorem Proving in Lean 4 for more information.

                                              Equations
                                              Instances For

                                                Step-wise reasoning over transitive relations.

                                                calc
                                                  a = b := pab
                                                  b = c := pbc
                                                  ...
                                                  y = z := pyz
                                                

                                                proves a = z from the given step-wise proofs. = can be replaced with any relation implementing the typeclass Trans. Instead of repeating the right- hand sides, subsequent left-hand sides can be replaced with _.

                                                calc
                                                  a = b := pab
                                                  _ = c := pbc
                                                  ...
                                                  _ = z := pyz
                                                

                                                It is also possible to write the first relation as <lhs>\n _ = <rhs> := <proof>. This is useful for aligning relation symbols, especially on longer: identifiers:

                                                calc abc
                                                  _ = bce := pabce
                                                  _ = cef := pbcef
                                                  ...
                                                  _ = xyz := pwxyz
                                                

                                                calc works as a term, as a tactic or as a conv tactic.

                                                See Theorem Proving in Lean 4 for more information.

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

                                                                                                                            Apply function extensionality and introduce new hypotheses. The tactic funext will keep applying the funext lemma until the goal target is not reducible to

                                                                                                                              |-  ((fun x => ...) = (fun x => ...))
                                                                                                                            

                                                                                                                            The variant funext h₁ ... hₙ applies funext n times, and uses the given identifiers to name the new hypotheses. Patterns can be used like in the intro tactic. Example, given a goal

                                                                                                                              |-  ((fun x : Nat × Bool => ...) = (fun x => ...))
                                                                                                                            

                                                                                                                            funext (a, b) applies funext once and performs pattern matching on the newly introduced pair.

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

                                                                                                                              Expands

                                                                                                                              class abbrev C <params> := D_1, ..., D_n
                                                                                                                              

                                                                                                                              into

                                                                                                                              class C <params> extends D_1, ..., D_n
                                                                                                                              attribute [instance] C.mk
                                                                                                                              
                                                                                                                              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

                                                                                                                                  · tac focuses on the main goal and tries to solve it using tac, or else fails.

                                                                                                                                  Equations
                                                                                                                                  Instances For

                                                                                                                                    Similar to first, but succeeds only if one the given tactics solves the current goal.

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

                                                                                                                                      repeat and while notation #

                                                                                                                                      inductive Lean.Loop :
                                                                                                                                      Instances For
                                                                                                                                        @[inline]
                                                                                                                                        def Lean.Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] :
                                                                                                                                        Lean.Loopβ(Unitβm (ForInStep β))m β
                                                                                                                                        Equations
                                                                                                                                        Instances For
                                                                                                                                          @[specialize #[]]
                                                                                                                                          partial def Lean.Loop.forIn.loop {β : Type u} {m : Type u → Type v} [Monad m] (f : Unitβm (ForInStep β)) (b : β) :
                                                                                                                                          m β
                                                                                                                                          instance Lean.instForInLoopUnit {m : Type u_1 → Type u_2} :
                                                                                                                                          Equations
                                                                                                                                          • Lean.instForInLoopUnit = { forIn := fun {β : Type u_1} [Monad m] => Lean.Loop.forIn }
                                                                                                                                          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

                                                                                                                                                    Unexpander for the { x } notation.

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

                                                                                                                                                      Unexpander for the { x, y, ... } notation.

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