Documentation

Aesop.Nanos

source
structure Aesop.Nanos :
Type
Instances For
    source
    instance Aesop.instInhabitedNanos :
    Inhabited Nanos
    Equations
      source
      instance Aesop.instBEqNanos :
      BEq Nanos
      Equations
        source
        instance Aesop.instOrdNanos :
        Ord Nanos
        Equations
          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
                        def Aesop.Nanos.printAsMillis (n : Nanos) :
                        String
                        Equations
                          Instances For