Documentation

Lean.Data.Json.Basic

Instances For
    Equations
      Instances For
        Equations
          Instances For
            Equations
              Instances For
                Equations
                  Instances For
                    Equations
                      Instances For
                        Equations
                          Instances For
                            Equations
                              Instances For
                                Equations
                                  Instances For

                                    Attempts to convert a float to a JsonNumber, if the number isn't finite returns the appropriate string from "NaN", "Infinity", "-Infinity".

                                    Equations
                                      Instances For
                                        def Lean.strLt (a b : String) :
                                        Equations
                                          Instances For
                                            inductive Lean.Json :
                                            Instances For
                                              Equations
                                                Equations
                                                  Instances For
                                                    instance Lean.Json.instOfNat {n : Nat} :
                                                    Equations
                                                      Equations
                                                        Instances For
                                                          Equations
                                                            Instances For
                                                              Equations
                                                                Instances For
                                                                  Equations
                                                                    Instances For
                                                                      Equations
                                                                        Instances For
                                                                          Equations
                                                                            Instances For
                                                                              Equations
                                                                                Instances For
                                                                                  Equations
                                                                                    Instances For
                                                                                      Equations
                                                                                        Instances For
                                                                                          Equations
                                                                                            Instances For
                                                                                              Equations
                                                                                                Instances For
                                                                                                  Equations
                                                                                                    Instances For

                                                                                                      Assuming both inputs o₁, o₂ are json objects, will compute {...o₁, ...o₂}. If o₁ is not a json object, o₂ will be returned.

                                                                                                      Equations
                                                                                                        Instances For
                                                                                                          Instances For