Version

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

structure Lake.SemVerCore : Type

The major-minor-patch triple of a SemVer.

• major : Nat
• minor : Nat
• patch : Nat

instance Lake.instInhabitedSemVerCore : Inhabited Lake.SemVerCore

Equations

• Lake.instInhabitedSemVerCore = { default := { major := default, minor := default, patch := default } }

instance Lake.instReprSemVerCore : Repr Lake.SemVerCore

Equations

• Lake.instReprSemVerCore = { reprPrec := Lake.reprSemVerCore✝ }

instance Lake.instDecidableEqSemVerCore : DecidableEq Lake.SemVerCore

Equations

• Lake.instDecidableEqSemVerCore = Lake.decEqSemVerCore✝

instance Lake.instOrdSemVerCore : Ord Lake.SemVerCore

Equations

• Lake.instOrdSemVerCore = { compare := Lake.ordSemVerCore✝ }

instance Lake.instLTSemVerCore : LT Lake.SemVerCore

Equations

• Lake.instLTSemVerCore = ltOfOrd

instance Lake.instLESemVerCore : LE Lake.SemVerCore

Equations

• Lake.instLESemVerCore = leOfOrd

instance Lake.instMinSemVerCore : Min Lake.SemVerCore

Equations

• Lake.instMinSemVerCore = minOfLe

instance Lake.instMaxSemVerCore : Max Lake.SemVerCore

Equations

• Lake.instMaxSemVerCore = maxOfLe

def Lake.SemVerCore.parse (ver : String) : Except String Lake.SemVerCore

Equations

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

def Lake.SemVerCore.toString (ver : Lake.SemVerCore) : String

Equations

• ver.toString = toString "" ++ toString ver.major ++ toString "." ++ toString ver.minor ++ toString "." ++ toString ver.patch ++ toString ""

instance Lake.instToStringSemVerCore : ToString Lake.SemVerCore

Equations

• Lake.instToStringSemVerCore = { toString := Lake.SemVerCore.toString }

instance Lake.instToJsonSemVerCore : Lean.ToJson Lake.SemVerCore

Equations

• Lake.instToJsonSemVerCore = { toJson := fun (x : Lake.SemVerCore) => Lean.Json.str x.toString }

instance Lake.instFromJsonSemVerCore : Lean.FromJson Lake.SemVerCore

Equations

• Lake.instFromJsonSemVerCore = { fromJson? := fun (x : Lean.Json) => do let __do_lift ← Lean.fromJson? x Lake.SemVerCore.parse __do_lift }

instance Lake.instToExprSemVerCore : Lean.ToExpr Lake.SemVerCore

Equations

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

structure Lake.StdVerextends Lake.SemVerCore : Type

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

• major : Nat
• minor : Nat
• patch : Nat
• specialDescr : String

instance Lake.instInhabitedStdVer : Inhabited Lake.StdVer

Equations

• Lake.instInhabitedStdVer = { default := { toSemVerCore := default, specialDescr := default } }

instance Lake.instReprStdVer : Repr Lake.StdVer

Equations

• Lake.instReprStdVer = { reprPrec := Lake.reprStdVer✝ }

instance Lake.instDecidableEqStdVer : DecidableEq Lake.StdVer

Equations

• Lake.instDecidableEqStdVer = Lake.decEqStdVer✝

@[reducible, inline]

abbrev Lake.LeanVer : Type

A Lean version.

Equations

• Lake.LeanVer = Lake.StdVer

instance Lake.instCoeStdVerSemVerCore : Coe Lake.StdVer Lake.SemVerCore

Equations

• Lake.instCoeStdVerSemVerCore = { coe := Lake.StdVer.toSemVerCore }

@[inline]

def Lake.StdVer.ofSemVerCore (ver : Lake.SemVerCore) : Lake.StdVer

Equations

• Lake.StdVer.ofSemVerCore ver = { toSemVerCore := ver, specialDescr := "" }

instance Lake.instCoeSemVerCoreStdVer : Coe Lake.SemVerCore Lake.StdVer

Equations

• Lake.instCoeSemVerCoreStdVer = { coe := Lake.StdVer.ofSemVerCore }

def Lake.StdVer.compare (a b : Lake.StdVer) : Ordering

Equations

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

instance Lake.instOrdStdVer : Ord Lake.StdVer

Equations

• Lake.instOrdStdVer = { compare := Lake.StdVer.compare }

instance Lake.instLTStdVer : LT Lake.StdVer

Equations

• Lake.instLTStdVer = ltOfOrd

instance Lake.instLEStdVer : LE Lake.StdVer

Equations

• Lake.instLEStdVer = leOfOrd

instance Lake.instMinStdVer : Min Lake.StdVer

Equations

• Lake.instMinStdVer = minOfLe

instance Lake.instMaxStdVer : Max Lake.StdVer

Equations

• Lake.instMaxStdVer = maxOfLe

def Lake.StdVer.parse (ver : String) : Except String Lake.StdVer

Equations

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

def Lake.StdVer.toString (ver : Lake.StdVer) : String

Equations

• ver.toString = if ver.specialDescr.isEmpty = true then ver.toString else toString "" ++ toString ver.toSemVerCore ++ toString "-" ++ toString ver.specialDescr ++ toString ""

instance Lake.instToStringStdVer : ToString Lake.StdVer

Equations

• Lake.instToStringStdVer = { toString := Lake.StdVer.toString }

instance Lake.instToJsonStdVer : Lean.ToJson Lake.StdVer

Equations

• Lake.instToJsonStdVer = { toJson := fun (x : Lake.StdVer) => Lean.Json.str x.toString }

instance Lake.instFromJsonStdVer : Lean.FromJson Lake.StdVer

Equations

• Lake.instFromJsonStdVer = { fromJson? := fun (x : Lean.Json) => do let __do_lift ← Lean.fromJson? x Lake.StdVer.parse __do_lift }

instance Lake.instToExprStdVer : Lean.ToExpr Lake.StdVer

Equations

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

Version Literals

Defines the v!"<ver>" syntax for version literals. The elaborator attempts to synthesize an instance of ToVersion for the expected type and then applies it to the string literal.

class Lake.DecodeVersion (α : Type u) : Type u

Parses a version from a string.

• decodeVersion : String → Except String α

instance Lake.instDecodeVersionSemVerCore : Lake.DecodeVersion Lake.SemVerCore

Equations

• Lake.instDecodeVersionSemVerCore = { decodeVersion := Lake.SemVerCore.parse }

@[defaultInstance 1000]

instance Lake.instDecodeVersionStdVer : Lake.DecodeVersion Lake.StdVer

Equations

• Lake.instDecodeVersionStdVer = { decodeVersion := Lake.StdVer.parse }

def Lake.verLit : Lean.ParserDescr

A Lake version literal.

Equations

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

def Lake.elabVerLit : Lean.Elab.Term.TermElab

Equations

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