Idris2Doc : Deriving.DepTyCheck.Util.ArgsPerm

Deriving.DepTyCheck.Util.ArgsPerm

(source)
Reexports
import public Data.List.Ex
import public Data.SortedMap
import public Data.Vect
import public Decidable.Equality
import public Language.Reflection
import public Language.Reflection.Syntax
import public Language.Reflection.Syntax.Ops
import public Syntax.IHateParens.List
import public Syntax.IHateParens.Vect
Definitions
orderIndices : Ord a => (xs : List a) -> Vect (xs .length) (Fin (xs .length))
  Totality: total
  Visibility: export
reorder : Vect n (Fin n) -> Vect n a -> Vect n a
  Totality: total
  Visibility: export
reorder' : (xs : List a) -> Vect (xs .length) (Fin (xs .length)) -> (ys : List a ** ys .length = xs .length)
  Totality: total
  Visibility: export
reorder'' : Maybe (n : Nat ** Vect n (Fin n)) -> List TTImp -> Maybe (List TTImp)
  Totality: total
  Visibility: export
reorderGend : Bool -> Vect n (Fin n) -> TTImp -> TTImp
  Produces expression returning a mkdpair in a different order, if needed
  
  Direct means that given expression which returns ascending order, result is permutated; non-direct means vice versa.

  Totality: total
  Visibility: export