def Std.Time.«termDatespec(_)» : Lean.ParserDescr

Syntax for defining a date spec at compile time.

Equations

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

def Std.Time.«termDatespec(_,_)» : Lean.ParserDescr

Syntax for defining a date spec and configuration of this date spec at compile time.

Equations

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

def Std.Time.formatStringToFormat (fmt : Lean.TSyntax `str) (config : Option (Lean.TSyntax `term)) : Lean.MacroM (Lean.TSyntax `term)

Equations

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