Idris2Doc : Misc

Misc

(source)
Definitions
constUnit : a -> ()
  Totality: total
  Visibility: public export
const2Unit : a -> b -> ()
  Totality: total
  Visibility: public export
fromBool : Num a => Bool -> a
  Totality: total
  Visibility: public export
applyWhen : Bool -> (a -> a) -> a -> a
  Totality: total
  Visibility: public export
updateAt : Eq a => (a -> b) -> (a, b) -> a -> b
  Totality: total
  Visibility: public export
graph : {t : a -> Type} -> ((x : a) -> t x) -> a -> (x : a ** t x)
  Graph of a dependent function

  Totality: total
  Visibility: public export
dependentMap : Functor f => {t : a -> Type} -> ((x : a) -> t x) -> f a -> f (x : a ** t x)
  Version of `map` for dependent function
  Note that here `x : a` is identity in some sense, it comes from `f a`

  Totality: total
  Visibility: public export
data IsNo : Dec a -> Type
  The proof that a decidable property leads to a contradiction
  `IsNo` is a type Idris can automatically synthesise, unlike `Not`
  See example below

  Totality: total
  Visibility: public export
  Constructor: 
ItIsNo : IsNo (No contra)

  Hint: 
{auto {conArg:18850} : DecEq a} -> IsNo (decEq x y) -> NotElem y [x]
isNoSym : {auto {conArg:11722} : DecEq a} -> IsNo (decEq x y) -> IsNo (decEq y x)
  Totality: total
  Visibility: public export
proofIneqIsNo : {auto {conArg:11829} : DecEq a} -> Not (x = y) -> IsNo (decEq x y)
  Proof of inequality yields IsNo

  Totality: total
  Visibility: public export
data IsNothing : Maybe a -> Type
  Totality: total
  Visibility: public export
  Constructor: 
ItIsNothing : IsNothing Nothing

  Hint: 
Uninhabited (IsNothing (Just x))
maybeVoidIsNothing : (x : Maybe Void) -> IsNothing x
  Totality: total
  Visibility: public export
data NotElem : DecEq a => a -> Vect n a -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
NotInEmptyVect : {auto {conArg:11972} : DecEq a} -> NotElem x []
  
NotInNonEmptyVect : {auto {conArg:11986} : DecEq a} -> (xs : Vect n a) -> IsNo (decEq x y) -> NotElem x xs => NotElem x (y :: xs)
notEqualNotElem : {auto {conArg:12024} : DecEq a} -> IsNo (decEq x y) -> NotElem x [y]
  Totality: total
  Visibility: public export
notElemSym : {auto {conArg:12075} : DecEq a} -> NotElem i [j] -> NotElem j [i]
  If an element `i` is not in the singleton list `[j]`, then `j` is not in
  the singleton list `[i]`

  Totality: total
  Visibility: public export
elemSym : DecEq a => Elem i [j] -> Elem j [i]
  If an element `i` is in the singleton list `[j]`, then `j` is in the 
  singleton list `[i]`

  Totality: total
  Visibility: public export
liftA2 : Applicative f => f a -> f b -> f (a, b)
  Definition of liftA2 in terms of (<*>)

  Totality: total
  Visibility: public export
strength : Applicative f => a -> f b -> f (a, b)
  Tensorial strength

  Totality: total
  Visibility: public export
toList' : Vect n a -> List a
  toList with a different foldable implementation

  Totality: total
  Visibility: public export
fromList' : (xs : List a) -> Vect (length xs) a
  Totality: total
  Visibility: public export
sum : Num a => Vect n a -> a
  Totality: total
  Visibility: public export
prod : Num a => Vect n a -> a
  Totality: total
  Visibility: public export
max : Ord a => Vect n a -> Maybe a
  Totality: total
  Visibility: public export
argmax : Ord a => IsSucc n => Vect n a -> Fin n
  Totality: total
  Visibility: public export
argmin : Ord a => IsSucc n => Vect n a -> Fin n
  Totality: total
  Visibility: public export
unConcat : Vect (n * m) a -> Vect n (Vect m a)
  Dual to concat from Data.Vect

  Totality: total
  Visibility: public export
dropFromEnd : Eq a => a -> Vect n a -> List a
  Trim a specified trailing value

  Totality: total
  Visibility: public export
consSnoc : Vect n a -> a -> a -> Vect (2 + n) a
  Combination of `cons` and `snoc`: adds an element in front, and at the end

  Totality: total
  Visibility: public export
padToSize : Vect size a -> (targetSize : Nat) -> a -> LTE size targetSize => Vect targetSize a
  Pad a vector with a specified element to exactly `targetSize`

  Totality: total
  Visibility: public export
drop : (i : Fin (S n)) -> Vect n a -> Vect (minus n (finToNat i)) a
  Drop the first i elements of a vector
  Analogous to Data.Vect.drop, except the index is Fin n instead of Nat

  Totality: total
  Visibility: public export
drop : DecEq a => (xs : Vect n a) -> (elem : Elem x xs) -> Vect (minus n (finToNat (FS (elemToFin elem)))) a
  Drop all the elements up and until the element `x` from a vector

  Totality: total
  Visibility: public export
sum : Num a => List a -> a
  Totality: total
  Visibility: public export
prod : Num a => List a -> a
  Totality: total
  Visibility: public export
listZip : List a -> List b -> List (a, b)
  Totality: total
  Visibility: public export
mapWithIndex : (Nat -> a -> b) -> List a -> List b
  Map each element along with its zero-based position in the list.

  Totality: total
  Visibility: public export
chunksOf : Nat -> List a -> List (List a)
  Split a list into consecutive chunks of size `n` (clamped to at least 1).
  The final chunk may be shorter than `n`, this is why the length of the
  list is needed as upper bound.

  Totality: total
  Visibility: public export
max : Ord a => List a -> Maybe a
  Totality: total
  Visibility: public export
max : Ord a => (xs : List a) -> NonEmpty xs => a
  Totality: total
  Visibility: public export
dropFromEnd : Eq a => a -> List a -> List a
  Trim a specified trailing value

  Totality: total
  Visibility: public export
consSnoc : List a -> a -> a -> List a
  Combination of `cons` and `snoc`: adds an element in front, and at the end

  Totality: total
  Visibility: public export
padToSize : Nat -> a -> List a -> List a
  Pad a list with a specified element to at least `targetSize`

  Totality: total
  Visibility: public export
dropAfterElem : (xs : List a) -> Elem x xs -> List a
  Drop all the elements after the element `x` from a list

  Totality: total
  Visibility: public export
cons : x -> (Fin l -> x) -> Fin (S l) -> x
  Analogue of `(::)`

  Totality: total
  Visibility: public export
head : (Fin (S l) -> x) -> x
  Totality: total
  Visibility: public export
tail : (Fin (S l) -> x) -> Fin l -> x
  Totality: total
  Visibility: public export
init : (Fin (S n) -> a) -> Fin n -> a
  All but the last element

  Totality: total
  Visibility: public export
takeFin : (s : Fin (S n)) -> Vect n a -> Vect (finToNat s) a
  Analogus to `Data.Vect.take`

  Totality: total
  Visibility: public export
sum : Num a => (Fin n -> a) -> a
  Totality: total
  Visibility: public export
prod : Num a => (Fin n -> a) -> a
  Totality: total
  Visibility: public export
toList : (Fin n -> a) -> List a
  Totality: total
  Visibility: public export
minusSuccLTE : LTE n m -> minus (S m) n = S (minus m n)
  Proof that subtracting from a successor is the same as taking the sucessor
  of the subtraction

  Totality: total
  Visibility: public export
weakenN' : (0 n : Nat) -> Fin m -> Fin (n + m)
  A version of `weakenN` from Data.Fin with `n` on the other side of `+`

  Totality: total
  Visibility: public export
weakenMultN : (m : Nat) -> IsSucc m => Fin n -> Fin (m * n)
  Variant of `weakenN` from `Data.Fin`, but for multiplication
  Like shiftMul, but without changing the value of the index

  Totality: total
  Visibility: public export
shiftMul : (stride : Nat) -> IsSucc stride => Fin n -> Fin (n * stride)
  Variant of `shift` from Data.Fin, but for multiplication
  Given a stride and an index `i : Fin n`, it returns a stride-sized step
  That is, it returns `stride * i` : Fin (stride * n)
  Implemented by recursing on i, adding stride each time

  Totality: total
  Visibility: public export
strengthenN : Fin (m + n) -> Either (Fin m) (Fin n)
  Analogue of `strengthen` from Data.Fin
  Attempts to strengthen the bound on Fin (m + n) to Fin m
  If it doesn't succeed, then returns the remainder in Fin n

  Totality: total
  Visibility: public export
finS' : Fin n -> Fin n
  Analogue of `finS` from `Data.Fin`, but without without wrapping
  That is, `finS' last = last`

  Totality: total
  Visibility: public export
lastBiggerThanOthers : (i : Fin (S n)) -> So (last >= i)
  This can be implemented using `Data.Fin.Order`, but it doesn't seem worth
  the effort, as the typechecker ends up needing a lot of extra hand holding

  Totality: total
  Visibility: public export
addFinsBounded : Fin n -> Fin n -> Fin n
  Adds two bounded numbers, bounds the result
  That is, `addFinsBounded {n=5} 3 4 = 4`
  `assert_smaller` is only needed for totality checking

  Totality: total
  Visibility: public export
half : Fin n -> Fin n
  Divides a Fin by 2, rounding down
  `half {n=10} 6 = 3`
  `half {n=10} 5 = 2`
  `half {n=10} 4 = 2`
  `half {n=10} 3 = 1`
  `half {n=10} 2 = 1`
  `half {n=10} 1 = 0`

  Totality: total
  Visibility: public export
mid : (low : Fin n) -> (high : Fin n) -> So (high >= low) => Fin n
  Computes the midway index between two bounds

  Totality: total
  Visibility: public export
multSucc : IsSucc m -> IsSucc n -> IsSucc (m * n)
  Totality: total
  Visibility: public export
allSuccThenProdSucc : (xs : List Nat) -> All IsSucc xs => IsSucc (prod xs)
  Totality: total
  Visibility: public export
findBinBetween : Ord a => IsSucc n => Vect n a -> a -> Range n -> Maybe (Fin n)
  Given a non-empty sorted vector `xs`, an element `x` and a lower and upper
  bound, it finds the "right bin", i.e. the index of the smallest element 
  between the bounds that's bigger than `x`
  If `x` is bigger than the largest element, returns `Nothing`
  `findBinBetween [2,7,10] 1 (MkRange 0 2) = Just 0`
  `findBinBetween [2,7,10] 3 (MkRange 0 2) = Just 1`
  `findBinBetween [2,7,10] 9 (MkRange 0 2) = Just 2`
  `findBinBetween [2,7,10] 7 (MkRange 0 2) = Just 2`
  `findbinbetween [2,7,15] 7 (MkRange 0 2) = Nothing`
  `findBinBetween [1,2,3,4,5] 6 (MkRange 0 4) = Nothing`
  Done using binary search

  Totality: total
  Visibility: public export
findBin : Ord a => IsSucc n => Vect n a -> a -> Maybe (Fin n)
  Todo can this eventually be generalised to non-cubical tensors?
  Given a non-empty sorted vector `xs` and an element `x` it finds the 
  "right bin", i.e. the index of the smallest element that's bigger than `x`
  If `x` is bigger than the highest element, returns `Nothing`
  `findBin [2,7,10] 1 = Just 0`
  `findBin [2,7,10] 3 = Just 1`
  `findBin [2,4,6,8] 7 = Just 3`

  Totality: total
  Visibility: public export
mkDepPairShow : Show a => ((x : a) -> Show (b x)) => DPair a b -> String
  Totality: total
  Visibility: public export
runIf : HasIO io => Bool -> io () -> io ()
  Totality: total
  Visibility: public export
pairIO : HasIO io => io a -> io b -> io (a, b)
  Totality: total
  Visibility: public export
rewriteAllMap : All p (f <$> xs) -> All (p . f) xs
  Totality: total
  Visibility: public export
rewriteAllMap' : All (p . f) xs -> All p (f <$> xs)
  Totality: total
  Visibility: public export
rewriteAllMap : All p (f <$> xs) -> All (p . f) xs
  Totality: total
  Visibility: public export
allToVect : All p (replicate n a) -> Vect n (p a)
  Cnvert an all to a vector if it's made out of replicated things

  Totality: total
  Visibility: public export
constantToVect : All (const b) xs -> Vect n b
  Totality: total
  Visibility: public export
dTraverse : Applicative f => ((p : pType) -> f (q p)) -> (xs : Vect n pType) -> f (All q xs)
  Dependent parametric traverse

  Totality: total
  Visibility: public export
record Iso : Type -> Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkIso : (forward : (a -> b)) -> (backward : (b -> a)) -> ((x : a) -> backward (forward x) = x) -> ((y : b) -> forward (backward y) = y) -> Iso a b

  Projections:
  
.backward : Iso a b -> b -> a
  
.backwardForward : ({rec:0} : Iso a b) -> (y : b) -> forward {rec:0} (backward {rec:0} y) = y
  
.forward : Iso a b -> a -> b
  
.forwardBackward : ({rec:0} : Iso a b) -> (x : a) -> backward {rec:0} (forward {rec:0} x) = x
.forward : Iso a b -> a -> b
  Totality: total
  Visibility: public export
forward : Iso a b -> a -> b
  Totality: total
  Visibility: public export
.backward : Iso a b -> b -> a
  Totality: total
  Visibility: public export
backward : Iso a b -> b -> a
  Totality: total
  Visibility: public export
.forwardBackward : ({rec:0} : Iso a b) -> (x : a) -> backward {rec:0} (forward {rec:0} x) = x
  Totality: total
  Visibility: public export
forwardBackward : ({rec:0} : Iso a b) -> (x : a) -> backward {rec:0} (forward {rec:0} x) = x
  Totality: total
  Visibility: public export
.backwardForward : ({rec:0} : Iso a b) -> (y : b) -> forward {rec:0} (backward {rec:0} y) = y
  Totality: total
  Visibility: public export
backwardForward : ({rec:0} : Iso a b) -> (y : b) -> forward {rec:0} (backward {rec:0} y) = y
  Totality: total
  Visibility: public export
index : (i : Fin k) -> All p ts -> p (index i ts)
  Totality: total
  Visibility: public export
testFun : Nat -> (m : Nat ** Vect m Nat)
filter2 : (a -> Bool) -> Vect len a -> Vect p a
  Totality: total
  Visibility: public export