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
      Instances For
        Equations
          Instances For
            structure Lake.StdVerextends Lake.SemVerCore :

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

            Instances For
              @[reducible, inline]

              A Lean version.

              Equations
                Instances For
                  @[inline]
                  Equations
                    Instances For
                      Equations
                        Instances For
                          Equations
                            Equations
                              Equations
                                Instances For
                                  Equations
                                    Instances For

                                      A Lean toolchain version.

                                      Instances For
                                        Equations
                                          Instances For
                                            Equations
                                              Instances For

                                                Parse a toolchain from a lean-toolchain file.

                                                Equations
                                                  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
                                                              Instances For
                                                                Equations
                                                                  Instances For
                                                                    Equations
                                                                      Equations
                                                                        Instances For
                                                                          Equations
                                                                            class Lake.DecodeVersion (α : Type u) :

                                                                            Parses a version from a string.

                                                                            Instances
                                                                              @[defaultInstance 1000]
                                                                              Equations