TyRE.Extra

Reexports

Definitions

extractBasedOnFst : (xs : List (a, b)) -> Elem x (map fst xs) -> b

Totality: total
Visibility: public export

extractBasedOnFstSpec : (xs : List a) -> (f : (a -> (b, c))) -> (x : b) -> (xInXs : Elem x (map fst (map f xs))) -> (e : a ** extractBasedOnFst (map f xs) xInXs = snd (f e))

Totality: total
Visibility: export

extractBasedOnFstAppLor : (xs : List (a, b)) -> (ys : List (a, b)) -> (x : a) -> (xInApp : Elem x (map fst (xs ++ ys))) -> Either (xInXs : Elem x (map fst xs) ** extractBasedOnFst (xs ++ ys) xInApp = extractBasedOnFst xs xInXs) (xInYs : Elem x (map fst ys) ** extractBasedOnFst (xs ++ ys) xInApp = extractBasedOnFst ys xInYs)

Totality: total
Visibility: export

replicate : Nat -> a -> SnocList a

Totality: total
Visibility: public export

replicateForSucc : (k : Nat) -> (elem : a) -> [<elem] ++ replicate k elem = replicate (S k) elem

Totality: total
Visibility: export

bindSpec : (f : (a -> List b)) -> (p : Pred b) -> (q : Pred a) -> ((x : a) -> (y : b ** (Elem y (f x), p y)) -> q x) -> (cs : List a) -> (y : b ** (Elem y (cs >>= f), p y)) -> (x : a ** (Elem x cs, (q x, (y : b ** (Elem y (f x), p y)))))

Totality: total
Visibility: export

mapSpec : (f : ((a, b) -> c)) -> (q : Pred (a, b)) -> (p : Pred c) -> (xs : List (a, b)) -> ((x1 : a) -> (x2 : b) -> p (f (x1, x2)) -> q (x1, x2)) -> (y : c) -> (Elem y (map f xs), p y) -> (x1 : a ** (x2 : b ** (prf : Elem x1 (map fst xs) ** (extractBasedOnFst xs prf = x2, (f (x1, x2) = y, q (x1, x2))))))

Totality: total
Visibility: export

biMapOnFst : (xs : List (a, c)) -> (f : (a -> b)) -> (g : (c -> d)) -> map fst (map (bimap f g) xs) = map f (map fst xs)

Totality: total
Visibility: export

elemMapRev : (xs : List a) -> (f : (a -> b)) -> Elem e (map f xs) -> (e' : a ** (Elem e' xs, f e' = e))

Totality: total
Visibility: export

eqForJust : Just x = Just y -> x = y

Totality: total
Visibility: export