Documentation

Lake.Config.OutFormat

inductive Lake.OutFormat :

Target output formats supported by the Lake CLI (e.g., lake query).

  • text : OutFormat

    Format target output as text.

  • json : OutFormat

    Format target output as JSON.

Instances For
    class Lake.ToText (α : Type u) :
    Instances
      @[instance 0]
      instance Lake.instToTextOfToString {α : Type u_1} [ToString α] :
      Equations
        instance Lake.instToTextList {α : Type u_1} [ToText α] :
        Equations
          instance Lake.instToTextArray {α : Type u_1} [ToText α] :
          Equations
            class Lake.FormatQuery (α : Type u) :

            Class used to format target output for lake query.

            Instances
              def Lake.nullFormat {α : Sort u_1} (fmt : OutFormat) :
              αString

              A format function that produces "null" output.

              Equations
                Instances For
                  @[instance 0]
                  instance Lake.instFormatQuery {α : Type u_1} :
                  Equations
                    @[specialize #[]]
                    def Lake.stdFormat {α : Type u_1} [ToText α] [Lean.ToJson α] (fmt : OutFormat) (a : α) :

                    Format function that uses ToText and ToJson to print output.

                    Equations
                      Instances For