Documentation

Std.Time.Notation.Spec

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

Syntax for defining a date spec at compile time.

Equations
    Instances For
      source
      def Std.Time.«termDatespec(_,_)» :
      Lean.ParserDescr

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

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