Idris2Doc : Data.Unique.Vect

Data.Unique.Vect

(source)
Definitions
data UniqueVect : (0 _ : Nat) -> (0 a : Type) -> DecEq a => Type
  A list with unique elements, length tracked statically
  An element can be inserted if it is not already in the list
  Like a Set, but with ordering
  @ a The type of the elements in the list

  Totality: total
  Visibility: public export
  Constructors:
  
Nil : {auto {conArg:16715} : DecEq a} -> UniqueVect 0 a
  
(::) : {auto {conArg:16728} : DecEq a} -> (x : a) -> (xs : UniqueVect n a) -> NotElem x xs => UniqueVect (S n) a
data NotElem : {auto {conArg:16750} : DecEq a} -> a -> UniqueVect n a -> Type
  A proof that an element is *not* found in the unique vector

  Totality: total
  Visibility: public export
  Constructors:
  
NotInEmptyVect : {auto {conArg:16766} : DecEq a} -> (x : a) -> NotElem x []
  
NotInNonEmptyVect : {auto de : DecEq a} -> (xs : UniqueVect n a) -> NotElem x xs -> IsNo (decEq x y) => {auto prf : NotElem y xs} -> NotElem x (y :: xs)

  Hint: 
{auto {conArg:18435} : DecEq a} -> IsNo (decEq x y) -> NotElem y [x]
data All : {auto {conArg:16835} : DecEq a} -> (0 _ : (a -> Type)) -> UniqueVect rank a -> Type
  A proof that elements of a unique vector satisfy a property

  Totality: total
  Visibility: public export
  Constructors:
  
Nil : {auto {conArg:16854} : DecEq a} -> All p []
  
(::) : {auto {conArg:16875} : DecEq a} -> {auto {conArg:16890} : NotElem x xs} -> p x -> All p xs -> All p (x :: xs)
data Elem : {auto {conArg:16929} : DecEq a} -> a -> UniqueVect n a -> Type
  A proof that an element is found in a vector with unique elements

  Totality: total
  Visibility: public export
  Constructors:
  
Here : {auto {conArg:16942} : DecEq a} -> {auto prf : NotElem x xs} -> Elem x (x :: xs)
  
There : {auto {conArg:16974} : DecEq a} -> {auto prf : NotElem y xs} -> Elem x xs -> Elem x (y :: xs)

  Hint: 
{auto {conArg:17016} : DecEq a} -> Uninhabited (Elem x [])
decElemInUniqueVect : {auto {conArg:17063} : DecEq a} -> (x : a) -> (xs : UniqueVect n a) -> Dec (Elem x xs)
  Decision procedure for unique vector's Elem

  Visibility: public export
notElem : {auto {conArg:17322} : DecEq a} -> Not (Elem x xs) -> NotElem x xs
  Visibility: public export
toVect : {auto {conArg:17462} : DecEq a} -> UniqueVect n a -> Vect n a
  Visibility: public export
fromVect : {auto {conArg:17502} : DecEq a} -> Vect n a -> (m : Nat ** UniqueVect m a)
  Converts a vector to a unique vector, removing duplicates if they exist

  Visibility: public export
indexOf : {auto {conArg:17639} : DecEq a} -> Elem x xs -> Fin n
  Turn the proof that an element `x` is in a vector into the index of `x`

  Visibility: public export
length : {auto {conArg:17708} : DecEq a} -> UniqueVect n a -> Nat
  Visibility: public export
drop : {auto {conArg:17750} : DecEq a} -> (xs : UniqueVect n a) -> (elem : Elem x xs) -> UniqueVect (minus n (finToNat (FS (indexOf elem)))) a
  Drop all the elements up and until the element `x` from a unique vector

  Visibility: public export
Test1 : UniqueVect 5 String
  Visibility: public export
wher : Elem "c" Test1
  Visibility: public export
removeIndex : {auto {conArg:18158} : DecEq a} -> UniqueVect (S n) a -> Fin (S n) -> UniqueVect n a
  Remove element from a unique vector at a given index

  Visibility: public export
removingElemIsStillNotElem : {auto {conArg:18175} : DecEq a} -> NotElem x xs => NotElem x (removeIndex xs i)
  Given a vector `xs` and a proof that `x` is not in `xs`, then even if
  we remove any elemens from `xs`, `x` will still not be in the result

  Visibility: public export
notEqualNotElem : {auto {conArg:18365} : DecEq a} -> IsNo (decEq x y) -> NotElem x [y]
  If `x` is not equal to `y`, then `x` is not in the list `[y]`
  It seems that Idris manages to discover this proof automatically, so 
  this is not needed in practice
  Its dual is needed, hence the %hint in for the declaration below

  Visibility: public export
notEqualNotElem2 : {auto {conArg:18435} : DecEq a} -> IsNo (decEq x y) -> NotElem y [x]
  Visibility: public export
numUnique : {auto {conArg:18496} : DecEq a} -> UniqueVect n a -> UniqueVect m a -> Nat
  Number of elements found in any of two unique vectors
  Effectively, union

  Visibility: public export
numOverlap : {auto {conArg:18617} : DecEq a} -> UniqueVect n a -> UniqueVect m a -> Nat
  Number of elements found in both of the two unique vectors
  Effectively, intersection

  Visibility: public export
numSymmetricDifference : {auto {conArg:18738} : DecEq a} -> UniqueVect n a -> UniqueVect m a -> Nat
  Number of elements that are found in one but not both of the two vectors
  Effectively, symmetric difference

  Visibility: public export
(+++) : {auto {conArg:18912} : DecEq a} -> (xs : UniqueVect n a) -> (ys : UniqueVect m a) -> UniqueVect (numUnique xs ys) a
  Union

  Visibility: public export
  Fixity Declaration: infixr operator, level 5
expandUnique : {auto {conArg:18931} : DecEq a} -> NotElem x xs => NotElem x ys => NotElem x (xs +++ ys)
  If `x` is not in `xs` nor `ys`, then it also won't be in `xs +++ ys`
intersect : {auto {conArg:19076} : DecEq a} -> (xs : UniqueVect n a) -> (ys : UniqueVect m a) -> UniqueVect (numOverlap xs ys) a
  Visibility: public export
notElemIntersect : {auto {conArg:19095} : DecEq a} -> NotElem x xs => Elem x ys => NotElem x (intersect xs ys)
  If `x` is not in `xs`, then we can intersect `xs` with any other list,
  and `x` still wont' be in the result (even if `x` was in the other list)
allElemIntersectFst : {auto {conArg:19235} : DecEq a} -> (xs : UniqueVect n a) -> (ys : UniqueVect m a) -> All (\x => Elem x xs) (intersect xs ys)
  All elements of the intersection of two vectors `xs` and `ys`
  will be elements of `xs`

  Visibility: public export
allElemIntersectSnd : {auto {conArg:19273} : DecEq a} -> (xs : UniqueVect n a) -> (ys : UniqueVect m a) -> All (\x => Elem x ys) (intersect xs ys)
  All elements of the intersection of two vectors `xs` and `ys`
  will be elements of `ys`

  Visibility: public export
symmetricDifference : {auto {conArg:19311} : DecEq a} -> (xs : UniqueVect n a) -> (ys : UniqueVect m a) -> UniqueVect (numSymmetricDifference xs ys) a
  Visibility: public export
l1 : UniqueVect 3 String
  Visibility: public export
l2 : UniqueVect 3 String
  Visibility: public export
l3 : UniqueVect 5 String
  Visibility: public export
l4 : UniqueVect 1 String
  Visibility: public export