sumR : Num a => Foldable f => f a -> a
Sum implemented with foldr
Visibility: public exportrecord VectHomomorphismProperty : {0 A : Type} -> {0 B : Type} -> (A -> B -> B) -> B -> (Vect n A -> B) -> Type
A function H : forall n. Vect n A -> B preserving the structure of vectors over A
Totality: total
Visibility: public export
Constructor: ShowVectHomomorphismProperty : {0 A : Type} -> {0 B : Type} -> {0 F : A -> B -> B} -> {0 E : B} -> {0 H : Vect n A -> B} -> H [] = E -> ((x : A) -> (xs : Vect n A) -> H (x :: xs) = F x (H xs)) -> VectHomomorphismProperty F E (\0 {n:3420} => H)
Projections:
.cons : {0 A : Type} -> {0 B : Type} -> {0 F : A -> B -> B} -> {0 E : B} -> {0 H : Vect n A -> B} -> VectHomomorphismProperty F E (\0 {n:3591} => H) -> (x : A) -> (xs : Vect n A) -> H (x :: xs) = F x (H xs)
.nil : {0 A : Type} -> {0 B : Type} -> {0 F : A -> B -> B} -> {0 E : B} -> {0 H : Vect n A -> B} -> VectHomomorphismProperty F E (\0 {n:3463} => H) -> H [] = E
.nil : {0 A : Type} -> {0 B : Type} -> {0 F : A -> B -> B} -> {0 E : B} -> {0 H : Vect n A -> B} -> VectHomomorphismProperty F E (\0 {n:3463} => H) -> H [] = E
- Visibility: public export
nil : {0 A : Type} -> {0 B : Type} -> {0 F : A -> B -> B} -> {0 E : B} -> {0 H : Vect n A -> B} -> VectHomomorphismProperty F E (\0 {n:3528} => H) -> H [] = E
- Visibility: public export
.cons : {0 A : Type} -> {0 B : Type} -> {0 F : A -> B -> B} -> {0 E : B} -> {0 H : Vect n A -> B} -> VectHomomorphismProperty F E (\0 {n:3591} => H) -> (x : A) -> (xs : Vect n A) -> H (x :: xs) = F x (H xs)
- Visibility: public export
cons : {0 A : Type} -> {0 B : Type} -> {0 F : A -> B -> B} -> {0 E : B} -> {0 H : Vect n A -> B} -> VectHomomorphismProperty F E (\0 {n:3671} => H) -> (x : A) -> (xs : Vect n A) -> H (x :: xs) = F x (H xs)
- Visibility: public export
Fixity Declaration: infixr operator, level 5 nilConsInitiality : (f : (a -> b -> b)) -> (e : b) -> (h1 : (Vect n a -> b)) -> (h2 : (Vect n a -> b)) -> VectHomomorphismProperty f e (\0 {n:3751} => h1) -> VectHomomorphismProperty f e (\0 {n:3763} => h2) -> (xs : Vect n a) -> h1 xs = h2 xs
There is an extensionally unique function preserving the vector structure
Visibility: exportfoldrVectHomomorphism : VectHomomorphismProperty f e (\0 {n:4159} => foldr f e)
Our tail-recursive foldr preserves the vector structure
Visibility: exportfoldrUniqueness : (h : (Vect n a -> b)) -> VectHomomorphismProperty f e (\0 {n:4359} => h) -> (xs : Vect n a) -> h xs = foldr f e xs
foldr is the unique function preserving the vector structure
Visibility: exportsumIsGTEtoParts : (xs : Vect n Nat) -> Elem x xs -> GTE (sumR xs) x
Each summand is `LTE` the sum
Visibility: exportsumMonotone : (xs : Vect n Nat) -> (ys : Vect n Nat) -> ((i : Fin n) -> LTE (index i xs) (index i ys)) -> LTE (sumR xs) (sumR ys)
`sumR : Vect n Nat -> Nat` is monotone
Visibility: export