Module Fin

Meta-data

Contents

data Fin : Nat -> Type where
    FZ : forall {k : Nat} . Fin (k + 1)
  ; FS : forall {k : Nat} . (Fin k) -> Fin (k + 1)
Representation of a number bounded above by n
upcast : forall {n : Nat, m : Nat} 
       . {m .≤ n} =>
    (Fin m) -> Fin n
If m < n then (x in Fin m) -> (x in Fin n)
fromN : forall {n : Nat, m : Nat} 
      . (N n) -> Fin (n + 1)
Map from a natural number into the finite set one bigger than it
fromNInto : forall {n : Nat, m : Nat} 
          . {m ≥ 1} =>
    (N n) -> Fin (n + m)
Map from a natural number into a finite set that is arbitrarily bigger than it