Misc

Definitions

data IsNo : Dec a -> Type

  IsNo is a type Idris can automatically synthesise, in contrast to
  in contrast to `Not (x = y)`

Totality: total
Visibility: public export
Constructor: 

ItIsNo : IsNo (No contra)

Hint: 

{auto {conArg:18435} : DecEq a} -> IsNo (decEq x y) -> NotElem y [x]

isNoSym : {auto {conArg:11389} : DecEq a} -> IsNo (decEq x y) -> IsNo (decEq y x)

  Can this be simplified?

Visibility: public export

proofIneqIsNo : {auto {conArg:11574} : DecEq a} -> Not (x = y) -> IsNo (decEq x y)

  Proof of inequality yields IsNo

Visibility: public export

liftA2 : Applicative f => f a -> f b -> f (a, b)

  Definition of liftA2 in terms of (<*>)

Visibility: public export

strength : Applicative f => a -> f b -> f (a, b)

  Tensorial strength

Visibility: public export

toList' : Vect n a -> List a

  toList with a different foldable implementation

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

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

Visibility: public export

data NotElem : DecEq a => a -> Vect n a -> Type

Totality: total
Visibility: public export
Constructors:

NotInEmptyVect : {auto {conArg:12477} : DecEq a} -> NotElem x []

NotInNonEmptyVect : {auto {conArg:12491} : DecEq a} -> (xs : Vect n a) -> IsNo (decEq x y) -> NotElem x xs => NotElem x (y :: xs)

notEqualNotElem : {auto {conArg:12529} : DecEq a} -> IsNo (decEq x y) -> NotElem x [y]

Visibility: public export

notElemSym : {auto {conArg:12580} : 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]`

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]`

Visibility: public export

cons : x -> (Fin l -> x) -> Fin (S l) -> x

  Analogue of `(::)`

Visibility: public export

head : (Fin (S l) -> x) -> x

Visibility: public export

tail : (Fin (S l) -> x) -> Fin l -> x

Visibility: public export

init : (Fin (S n) -> a) -> Fin n -> a

  All but the last element

Visibility: public export

takeFin : (s : Fin (S n)) -> Vect n a -> Vect (finToNat s) a

  Analogus to `Data.Vect.take`

Visibility: public export

sum : Num a => Vect n a -> a

Visibility: public export

prod : Num a => Vect n a -> a

Visibility: public export

argmax : Ord a => IsSucc n => Vect n a -> Fin n

Visibility: public export

argmin : Ord a => IsSucc n => Vect n a -> Fin n

Visibility: public export

unConcat : Vect (n * m) a -> Vect n (Vect m a)

  Dual to concat from Data.Vect

Visibility: public export

sum : Num a => List a -> a

Visibility: public export

prod : Num a => List a -> a

Visibility: public export

listZip : List a -> List b -> List (a, b)

Visibility: public export

maxInList : Ord a => List a -> Maybe a

Visibility: public export

weakenN' : (0 n : Nat) -> Fin m -> Fin (n + m)

  Like weakenN from Data.Fin, but where n is on the other side of +

Visibility: public export

weakenMultN : (m : Nat) -> IsSucc m => Fin n -> Fin (m * n)

  Like weakenN, but with mutliplication
  Like shiftMul, but without changing the value of the index

Visibility: public export

shiftMul : (stride : Nat) -> IsSucc stride => Fin n -> Fin (n * stride)

  Variant of `shift` from Data.Fin, but with multiplication
  Given an index i : Fin n, it recasts it as one where steps are stride sized
  That is, returns stride * i : Fin (stride * n)
  Implemented by recursing on i, adding stride each time

Visibility: public export

strengthenN : Fin (m + n) -> Either (Fin m) (Fin n)

  Analogous to 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

Visibility: public export

finS' : Fin n -> Fin n

  Like finS, but without wrapping
  finS' last = last

Visibility: public export

addFinsBounded : Fin n -> Fin n -> Fin n

  Adds two Fin n, and bounds the result
  Meaning (93:Fin 5) + (4 : Fin 5) = 4

Visibility: public export

half : Fin n -> Fin n

  Divides a Fin by 2, rounding down

Visibility: public export

mid : (low : Fin n) -> (high : Fin n) -> So (high >= low) => Fin n

  Computes the midway index between two bounds

Visibility: public export

findBinBetween : Ord a => Vect (S n) a -> a -> (lowInd : Fin (S n)) -> (highInd : Fin (S n)) -> So (highInd >= lowInd) => Maybe (Fin (S n))

  Given a non-empty sorted vector `xs`, finds the "right bin", i.e. the index 
  of the smallest element between the bounds that `x` is not bigger than.
  If `x` is bigger than the highest element, returns `Nothing`
  `findBinBetween [2,7,10] 1 0 2 = Just 0`
  `findBinBetween [2,7,10] 3 0 2 = Just 1`
  `findBinBetween [2,7,10] 9 0 2 = Just 2`
  `findBinBetween [2,7,10] 7 0 2 = Just 2`
  `findBinBetween [1,2,3,4,5] 6 0 4 = Nothing`

Visibility: public export

findBin : Ord a => Vect (S n) a -> a -> Maybe (Fin (S n))

  Todo can this eventually be generalised to non-cubical tensors?
  Given a non-empty sorted vector `xs`, finds the "right bin", i.e. the index 
  of the smallest element between the bounds that `x` is not bigger than.
  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`

Visibility: public export

mkDepPairShow : Show a => ((x : a) -> Show (b x)) => DPair a b -> String

Visibility: public export

interface Display : Type -> Type

  Interface describing how a type can be displayed as a 2d grid of characters

Parameters: a
Methods:

display : a -> (h : Nat ** (w : Nat ** Vect h (Vect w Char)))

Implementation: 

Display a => Display (RoseTreeSame a)

display : Display a => a -> (h : Nat ** (w : Nat ** Vect h (Vect w Char)))

Visibility: public export

runIf : HasIO io => Bool -> io () -> io ()

Visibility: public export

pairIO : HasIO io => io a -> io b -> io (a, b)

Visibility: public export

multFin : Fin m -> Fin n -> Fin (m * n)

  There is a similar function in Data.Fin.Arith, which has the smallest
  possible bound. This one does not, but has a simpler type signature.

Visibility: public export

splitList : Eq a => List a -> List a -> (n : Nat ** Vect n (List a))

  Splits xs at each occurence of delimeter (general version for lists)

Visibility: public export

splitString : String -> String -> (n : Nat ** Vect n String)

  Splits xs at each occurence of delimeter (string version)

Visibility: public export

replaceString : String -> String -> String -> String

  Simple string replacement function

Visibility: public export

constUnit : a -> ()

Visibility: public export

const2Unit : a -> b -> ()

Visibility: public export

fromBool : Num a => Bool -> a

Visibility: public export

applyWhen : Bool -> (a -> a) -> a -> a

Visibility: public export

rewriteAllMap : All p (f <$> xs) -> All (p . f) xs

Visibility: public export

rewriteAllMap' : All (p . f) xs -> All p (f <$> xs)

Visibility: public export

rewriteAllMap : All p (f <$> xs) -> All (p . f) xs

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

Visibility: public export

constantToVect : All (const b) xs -> Vect n b

Visibility: public export

dTraverse : Applicative f => ((p : pType) -> f (q p)) -> (xs : Vect n pType) -> f (All q xs)

  Dependent parametric traverse

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

Visibility: public export

forward : Iso a b -> a -> b

Visibility: public export

.backward : Iso a b -> b -> a

Visibility: public export

backward : Iso a b -> b -> a

Visibility: public export

.forwardBackward : ({rec:0} : Iso a b) -> (x : a) -> backward {rec:0} (forward {rec:0} x) = x

Visibility: public export

forwardBackward : ({rec:0} : Iso a b) -> (x : a) -> backward {rec:0} (forward {rec:0} x) = x

Visibility: public export

.backwardForward : ({rec:0} : Iso a b) -> (y : b) -> forward {rec:0} (backward {rec:0} y) = y

Visibility: public export

backwardForward : ({rec:0} : Iso a b) -> (y : b) -> forward {rec:0} (backward {rec:0} y) = y

Visibility: public export

multSucc : IsSucc m -> IsSucc n -> IsSucc (m * n)

Visibility: public export

allSuccThenProdSucc : (xs : List Nat) -> All IsSucc xs => IsSucc (prod xs)

Visibility: public export

updateAt : Eq a => (a -> b) -> (a, b) -> a -> b

Visibility: public export

graph : {t : a -> Type} -> ((x : a) -> t x) -> a -> (x : a ** t x)

  Graph of a dependent function

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`

Visibility: public export

index : (i : Fin k) -> All p ts -> p (index i ts)

Visibility: public export