Documentation

Aesop.Nanos

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