Documentation

Aesop.Nanos

source
structure Aesop.Nanos :
Type
Instances For
    source
    def Aesop.instInhabitedNanos.default :
    Nanos
    Equations
      Instances For
        source
        instance Aesop.instInhabitedNanos :
        Inhabited Nanos
        Equations
          source
          instance Aesop.instBEqNanos :
          BEq Nanos
          Equations
            source
            def Aesop.instBEqNanos.beq :
            Nanos → Nanos → Bool
            Equations
              Instances For
                source
                instance Aesop.instOrdNanos :
                Ord Nanos
                Equations
                  source
                  def Aesop.instOrdNanos.ord :
                  Nanos → Nanos → Ordering
                  Equations
                    Instances For
                      source
                      instance Aesop.Nanos.instOfNat {n : Nat} :
                      OfNat Nanos n
                      Equations
                        source
                        instance Aesop.Nanos.instLT :
                        LT Nanos
                        Equations
                          source
                          instance Aesop.Nanos.instDecidableRelLt :
                          DecidableRel fun (x1 x2 : Nanos) => x1 < x2
                          Equations
                            source
                            instance Aesop.Nanos.instLE :
                            LE Nanos
                            Equations
                              source
                              instance Aesop.Nanos.instDecidableRelLe :
                              DecidableRel fun (x1 x2 : Nanos) => x1 ≤ x2
                              Equations
                                source
                                instance Aesop.Nanos.instAdd :
                                Add Nanos
                                Equations
                                  source
                                  instance Aesop.Nanos.instHDivNat :
                                  HDiv Nanos Nat Nanos
                                  Equations
                                    source
                                    instance Aesop.Nanos.instToJson :
                                    Lean.ToJson Nanos
                                    Equations
                                      source
                                      def Aesop.Nanos.printAsMillis (n : Nanos) :
                                      String
                                      Equations
                                        Instances For