Version Literals

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

def Lake.DSL.SemVerCore.toExpr (self : SemVerCore) : Lean.Expr

Equations

• Lake.DSL.SemVerCore.toExpr self = Lean.mkApp3 (Lean.mkConst `Lake.SemVerCore.mk) (Lean.toExpr self.major) (Lean.toExpr self.minor) (Lean.toExpr self.patch)

@[implicit_reducible]

instance Lake.DSL.instToExprSemVerCore : Lean.ToExpr SemVerCore

Equations

• Lake.DSL.instToExprSemVerCore = { toExpr := Lake.DSL.SemVerCore.toExpr, toTypeExpr := Lean.mkConst `Lake.SemVerCore }

def Lake.DSL.StdVer.toExpr (self : StdVer) : Lean.Expr

Equations

• Lake.DSL.StdVer.toExpr self = Lean.mkApp2 (Lean.mkConst `Lake.StdVer.mk) (Lean.toExpr self.toSemVerCore) (Lean.toExpr self.specialDescr)

@[implicit_reducible]

instance Lake.DSL.instToExprStdVer : Lean.ToExpr StdVer

Equations

• Lake.DSL.instToExprStdVer = { toExpr := Lake.DSL.StdVer.toExpr, toTypeExpr := Lean.mkConst `Lake.StdVer }

def Lake.DSL.ComparatorOp.toExpr (self : ComparatorOp) : Lean.Expr

Equations

• Lake.DSL.ComparatorOp.toExpr Lake.ComparatorOp.lt = Lean.mkConst `Lake.ComparatorOp.lt
• Lake.DSL.ComparatorOp.toExpr Lake.ComparatorOp.le = Lean.mkConst `Lake.ComparatorOp.le
• Lake.DSL.ComparatorOp.toExpr Lake.ComparatorOp.gt = Lean.mkConst `Lake.ComparatorOp.gt
• Lake.DSL.ComparatorOp.toExpr Lake.ComparatorOp.ge = Lean.mkConst `Lake.ComparatorOp.ge
• Lake.DSL.ComparatorOp.toExpr Lake.ComparatorOp.eq = Lean.mkConst `Lake.ComparatorOp.eq
• Lake.DSL.ComparatorOp.toExpr Lake.ComparatorOp.ne = Lean.mkConst `Lake.ComparatorOp.ne

@[implicit_reducible]

instance Lake.DSL.instToExprComparatorOp : Lean.ToExpr ComparatorOp

Equations

• Lake.DSL.instToExprComparatorOp = { toExpr := Lake.DSL.ComparatorOp.toExpr, toTypeExpr := Lean.mkConst `Lake.ComparatorOp }

def Lake.DSL.VerComparator.toExpr (self : VerComparator) : Lean.Expr

Equations

• Lake.DSL.VerComparator.toExpr self = Lean.mkApp3 (Lean.mkConst `Lake.VerComparator.mk) (Lean.toExpr self.ver) (Lean.toExpr self.op) (Lean.toExpr self.includeSuffixes)

@[implicit_reducible]

instance Lake.DSL.instToExprVerComparator : Lean.ToExpr VerComparator

Equations

• Lake.DSL.instToExprVerComparator = { toExpr := Lake.DSL.VerComparator.toExpr, toTypeExpr := Lean.mkConst `Lake.VerComparator }

def Lake.DSL.VerRange.toExpr (self : VerRange) : Lean.Expr

Equations

• Lake.DSL.VerRange.toExpr self = Lean.mkApp2 (Lean.mkConst `Lake.VerRange.mk) (Lean.toExpr self.toString) (Lean.toExpr self.clauses)

@[implicit_reducible]

instance Lake.DSL.instToExprVerRange : Lean.ToExpr VerRange

Equations

• Lake.DSL.instToExprVerRange = { toExpr := Lake.DSL.VerRange.toExpr, toTypeExpr := Lean.mkConst `Lake.VerRange }

def Lake.DSL.InputVer.toExpr (self : InputVer) : Lean.Expr

Equations

• Lake.DSL.InputVer.toExpr Lake.InputVer.none = Lean.mkConst `Lake.InputVer.none
• Lake.DSL.InputVer.toExpr (Lake.InputVer.git rev) = Lean.mkApp (Lean.mkConst `Lake.InputVer.git) (Lean.toExpr rev)
• Lake.DSL.InputVer.toExpr (Lake.InputVer.ver ver) = Lean.mkApp (Lean.mkConst `Lake.InputVer.ver) (Lean.toExpr ver)

@[implicit_reducible]

instance Lake.DSL.instToExprInputVer : Lean.ToExpr InputVer

Equations

• Lake.DSL.instToExprInputVer = { toExpr := Lake.DSL.InputVer.toExpr, toTypeExpr := Lean.mkConst `Lake.InputVer }

def Lake.DSL.toResultExpr {α : Type} [Lean.ToExpr α] (x : Except String α) : Except String Lean.Expr

Equations

• Lake.DSL.toResultExpr x = Lean.toExpr <$> x