Documentation

Batteries.Data.Fin.Basic

def Fin.clamp (n : Nat) (m : Nat) :
Fin (m + 1)

min n m as an element of Fin (m + 1)

Equations
Instances For
    def Fin.enum (n : Nat) :

    enum n is the array of all elements of Fin n in order

    Equations
    Instances For
      def Fin.list (n : Nat) :
      List (Fin n)

      list n is the list of all elements of Fin n in order

      Equations
      Instances For