Utils.Misc

Definitions

Eithers : List Type -> Type

  primarily used for `hack_*` functions for hacking open ADTs into sums ^/v products

Visibility: public export

kill_linear : Void -> (1 _ : a) -> s

Visibility: public export

pair_to_list : (a, a) -> List a

Visibility: public export

vect_to_pair : Vect 2 a -> (a, a)

Visibility: public export

pair_to_vect : (a, a) -> Vect 2 a

Visibility: public export

from_vect : Vect 1 a -> a

Visibility: public export

to_vect : a -> Vect 1 a

Visibility: public export

s_and : Bool -> Bool -> Bool

  strict version of `(&&)`

Visibility: public export

mmod : Integer -> (m : Nat) -> {auto 0 _ : NonZero m} -> Nat

Visibility: public export

mod' : Integer -> Integer -> Integer

Visibility: public export

s_eq : (Bits b, Eq b) => Vect n b -> Vect n b -> Bool

Visibility: public export

s_eq' : (Bits b, Eq b) => List b -> List b -> Bool

Visibility: public export

vect_zip_with : (a -> b -> c) -> Vect n a -> Vect m b -> Vect (minimum n m) c

Visibility: public export

group : (n : Nat) -> (m : Nat) -> Vect (n * m) a -> Vect n (Vect m a)

Visibility: public export

chunk : Nat -> List a -> List (List a)

Visibility: public export

group' : (n : Nat) -> (m : Nat) -> Vect (n * m) a -> Vect m (Vect n a)

Visibility: public export

split_at_concat_rev : (n : Nat) -> (xs : Vect (n + m) a) -> (0 _ : splitAt n xs = (l, r)) -> l ++ r = xs

Visibility: export

concat_group_id : (n : Nat) -> (m : Nat) -> (v : Vect (n * m) a) -> concat (group n m v) = v

Visibility: public export

pow_mod : Integer -> Integer -> Integer -> Integer

Visibility: public export

mul_mod : Integer -> Integer -> Integer -> Integer

Visibility: public export

quot_rem : Integer -> Integer -> (Integer, Integer)

Visibility: public export

gcd' : Integer -> Integer -> Integer

Visibility: public export

are_coprimes : Integer -> Integer -> Bool

Visibility: public export

extended_gcd : Integer -> Integer -> (Integer, Integer)

Visibility: public export

inv_mul_mod : Integer -> Integer -> Integer

Visibility: public export

forM : Applicative f => (n : Nat) -> f b -> f (Vect n b)

Visibility: public export

utf8_decode : List Bits8 -> Maybe String

Visibility: public export

stream_concat : Foldable t => Stream (t a) -> Stream a

Visibility: public export

ok_minus : (n : Nat) -> (m : Nat) -> LTE m n -> Nat

Visibility: public export

enumerate : Nat -> List a -> List (Nat, a)

Visibility: public export

replace_vect : (0 _ : n = m) -> Vect n a -> Vect m a

Visibility: public export

cycle : Vect (S n) a -> Stream a

Visibility: public export

prepend : List a -> Stream a -> Stream a

Visibility: public export

duplicate : Stream a -> Stream (Stream a)

Visibility: public export

split : (n : Nat) -> Stream a -> (Vect n a, Stream a)

Visibility: public export

chunk : (n : Nat) -> Stream a -> Stream (Vect n a)

Visibility: public export

lte_plus_left : (a : Nat) -> LTE (a + b) c -> LTE b c

Visibility: public export

maybe_to_either : Maybe a -> Lazy b -> Either b a

Visibility: public export

init' : List a -> List a

Visibility: public export

uncons1 : List1 a -> (List a, a)

Visibility: public export

splitAt : (n : Nat) -> Stream a -> (Vect n a, Stream a)

Visibility: public export

zeros : Vect n Bits8

Visibility: public export

splitLastAt1 : (n : Nat) -> List a -> Maybe (List1 a, Vect n a)

Visibility: public export

modFinNZ : Nat -> (b : Nat) -> NonZero b -> Fin b

Visibility: public export

collapse_ordering : List Ordering -> Ordering

Visibility: public export

pad_zero : Nat -> List Bits8 -> List Bits8

Visibility: public export

splitAtExact : (n : Nat) -> List a -> Maybe (Vect n a, List a)

Visibility: public export