Documentation

Lake.Util.Version

Version #

This module contains useful definitions for manipulating versions. It also defines a v!"<ver>" syntax for version literals.

The major-minor-patch triple of a SemVer.

Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def Lake.instDecidableEqSemVerCore.decEq (x✝ x✝¹ : SemVerCore) :
      Decidable (x✝ = x✝¹)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            structure Lake.StdVerextends Lake.SemVerCore :

            A Lean-style semantic version. A major-minor-patch triple with an optional arbitrary - suffix.

            Instances For
              Equations
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def Lake.instDecidableEqStdVer.decEq (x✝ x✝¹ : StdVer) :
                  Decidable (x✝ = x✝¹)
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[reducible, inline]

                    A Lean version.

                    Equations
                    Instances For
                      @[inline]
                      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

                            A Lean toolchain version.

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

                                      Parse a toolchain from a lean-toolchain file.

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

                                        The elan toolchain file name (i.e., lean-toolchain).

                                        Equations
                                        Instances For
                                          @[inline]

                                          Parse a toolchain from the lean-toolchain file of the directory dir.

                                          Equations
                                          Instances For
                                            Equations
                                            class Lake.DecodeVersion (α : Type u) :

                                            Parses a version from a string.

                                            Instances