Idris2Doc : Control.Permutation.Types

Control.Permutation.Types

data Permutation : Nat -> Type
  This is something like `Vector k a`, except we restrict ourselves to only 1,...,n for `Permutation n`.

  Totality: total
  Constructors:
  
Nil : Permutation 0
  
(:*) : Fin (S n) -> Permutation n -> Permutation (S n)
debug : Permutation n -> String
  Totality: total
invert : Permutation n -> Permutation n
  Totality: total
toVector : Permutation n -> Vect n (Fin n)
  Totality: total