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.

instance Lake.DSL.instToExprSemVerCore : Lean.ToExpr SemVerCore

Equations

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

instance Lake.DSL.instToExprStdVer : Lean.ToExpr StdVer

Equations

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

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

Equations

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