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.instToExprSemVerCore : Lean.ToExpr SemVerCore

Equations

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

instance Lake.instToExprStdVer : Lean.ToExpr StdVer

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.