From dc16b72b04a2040fdf972c45d80e0fc2ee77b3e7 Mon Sep 17 00:00:00 2001 From: janmasrovira Date: Tue, 23 Jul 2024 15:19:41 +0000 Subject: [PATCH] deploy: 5bdd7868d70271818c1ef6c1069f7f6db0794bff --- Juvix.Builtin.V1.Bool-src.html | 2 +- Juvix.Builtin.V1.Fixity-src.html | 2 +- Juvix.Builtin.V1.List-src.html | 2 +- Juvix.Builtin.V1.Maybe-src.html | 2 +- Juvix.Builtin.V1.Nat-src.html | 2 +- Juvix.Builtin.V1.Nat.Base-src.html | 2 +- Juvix.Builtin.V1.String-src.html | 2 +- Juvix.Builtin.V1.Trait.Natural-src.html | 2 +- Stdlib.Cairo.Poseidon-src.html | 2 +- Stdlib.Data.Bool-src.html | 2 +- Stdlib.Data.Bool.Base-src.html | 2 +- Stdlib.Data.Field-src.html | 2 +- Stdlib.Data.Field.Base-src.html | 2 +- Stdlib.Data.Fixity-src.html | 2 +- Stdlib.Data.Int-src.html | 2 +- Stdlib.Data.Int.Base-src.html | 2 +- Stdlib.Data.Int.Ord-src.html | 2 +- Stdlib.Data.List-src.html | 50 ++++++++++++++-------- Stdlib.Data.List.Base-src.html | 26 +++++------ Stdlib.Data.List.Base.html | 2 +- Stdlib.Data.List.html | 12 +++--- Stdlib.Data.Maybe-src.html | 2 +- Stdlib.Data.Maybe.Base-src.html | 2 +- Stdlib.Data.Nat-src.html | 2 +- Stdlib.Data.Nat.Base-src.html | 2 +- Stdlib.Data.Nat.Ord-src.html | 2 +- Stdlib.Data.Pair-src.html | 2 +- Stdlib.Data.Pair.Base-src.html | 2 +- Stdlib.Data.Result-src.html | 2 +- Stdlib.Data.Result.Base-src.html | 2 +- Stdlib.Data.String-src.html | 2 +- Stdlib.Data.String.Base-src.html | 4 +- Stdlib.Data.String.Ord-src.html | 2 +- Stdlib.Data.Unit-src.html | 10 ++++- Stdlib.Data.Unit.html | 3 +- Stdlib.Debug.Fail-src.html | 2 +- Stdlib.Function-src.html | 2 +- Stdlib.Prelude-src.html | 2 +- Stdlib.System.IO-src.html | 2 +- Stdlib.System.IO.Base-src.html | 2 +- Stdlib.System.IO.Bool-src.html | 2 +- Stdlib.System.IO.Int-src.html | 2 +- Stdlib.System.IO.Nat-src.html | 2 +- Stdlib.System.IO.String-src.html | 2 +- Stdlib.Trait-src.html | 3 +- Stdlib.Trait.DivMod-src.html | 2 +- Stdlib.Trait.Eq-src.html | 2 +- Stdlib.Trait.Foldable-src.html | 6 +++ Stdlib.Trait.Foldable.Monomorphic-src.html | 50 ++++++++++++++++++++++ Stdlib.Trait.Foldable.Monomorphic.html | 26 +++++++++++ Stdlib.Trait.Foldable.Polymorphic-src.html | 40 +++++++++++++++++ Stdlib.Trait.Foldable.Polymorphic.html | 24 +++++++++++ Stdlib.Trait.Foldable.html | 2 + Stdlib.Trait.Functor-src.html | 2 +- Stdlib.Trait.Functor.Monomorphic-src.html | 2 +- Stdlib.Trait.Functor.Polymorphic-src.html | 2 +- Stdlib.Trait.Integral-src.html | 2 +- Stdlib.Trait.Natural-src.html | 2 +- Stdlib.Trait.Numeric-src.html | 2 +- Stdlib.Trait.Ord-src.html | 2 +- Stdlib.Trait.Partial-src.html | 2 +- Stdlib.Trait.Show-src.html | 2 +- Stdlib.Trait.html | 2 +- index-src.html | 2 +- index.html | 2 +- 65 files changed, 266 insertions(+), 94 deletions(-) create mode 100644 Stdlib.Trait.Foldable-src.html create mode 100644 Stdlib.Trait.Foldable.Monomorphic-src.html create mode 100644 Stdlib.Trait.Foldable.Monomorphic.html create mode 100644 Stdlib.Trait.Foldable.Polymorphic-src.html create mode 100644 Stdlib.Trait.Foldable.Polymorphic.html create mode 100644 Stdlib.Trait.Foldable.html diff --git a/Juvix.Builtin.V1.Bool-src.html b/Juvix.Builtin.V1.Bool-src.html index dc65e894..16496169 100644 --- a/Juvix.Builtin.V1.Bool-src.html +++ b/Juvix.Builtin.V1.Bool-src.html @@ -6,4 +6,4 @@ type Bool := | true | false; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Juvix.Builtin.V1.Fixity-src.html b/Juvix.Builtin.V1.Fixity-src.html index b317b79b..8225a324 100644 --- a/Juvix.Builtin.V1.Fixity-src.html +++ b/Juvix.Builtin.V1.Fixity-src.html @@ -23,4 +23,4 @@ syntax fixity composition := binary {assoc := right; above := [multiplicative]}; syntax fixity lcomposition := binary {assoc := left; above := [multiplicative]}; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Juvix.Builtin.V1.List-src.html b/Juvix.Builtin.V1.List-src.html index 74ba17cb..c56c04d7 100644 --- a/Juvix.Builtin.V1.List-src.html +++ b/Juvix.Builtin.V1.List-src.html @@ -11,4 +11,4 @@ nil | --- An element followed by a list :: a (List a); -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Juvix.Builtin.V1.Maybe-src.html b/Juvix.Builtin.V1.Maybe-src.html index 7cb15c84..3f1d9b92 100644 --- a/Juvix.Builtin.V1.Maybe-src.html +++ b/Juvix.Builtin.V1.Maybe-src.html @@ -7,4 +7,4 @@ type Maybe A := | nothing | just A; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Juvix.Builtin.V1.Nat-src.html b/Juvix.Builtin.V1.Nat-src.html index 084a5798..b72963b2 100644 --- a/Juvix.Builtin.V1.Nat-src.html +++ b/Juvix.Builtin.V1.Nat-src.html @@ -13,4 +13,4 @@ * := (Nat.*); fromNat (x : Nat) : Nat := x }; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Juvix.Builtin.V1.Nat.Base-src.html b/Juvix.Builtin.V1.Nat.Base-src.html index 9328c4cc..54b4834a 100644 --- a/Juvix.Builtin.V1.Nat.Base-src.html +++ b/Juvix.Builtin.V1.Nat.Base-src.html @@ -46,4 +46,4 @@ --- Modulo for ;Nat;s. builtin nat-mod mod (n m : Nat) : Nat := sub n (div n m * m); -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Juvix.Builtin.V1.String-src.html b/Juvix.Builtin.V1.String-src.html index 28191e4c..562c1890 100644 --- a/Juvix.Builtin.V1.String-src.html +++ b/Juvix.Builtin.V1.String-src.html @@ -11,4 +11,4 @@ --- Concatenation of two ;String;s. builtin string-concat axiom ++str : String -> String -> String; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Juvix.Builtin.V1.Trait.Natural-src.html b/Juvix.Builtin.V1.Trait.Natural-src.html index 4b892232..7774b3fa 100644 --- a/Juvix.Builtin.V1.Trait.Natural-src.html +++ b/Juvix.Builtin.V1.Trait.Natural-src.html @@ -18,4 +18,4 @@ }; open Natural public; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Cairo.Poseidon-src.html b/Stdlib.Cairo.Poseidon-src.html index beba96e5..94954574 100644 --- a/Stdlib.Cairo.Poseidon-src.html +++ b/Stdlib.Cairo.Poseidon-src.html @@ -40,4 +40,4 @@ (poseidonHash acc@PoseidonState{ s0 := s0 + x1; s1 := s1 + x2 }) xs; in PoseidonState.s0 (go (mkPoseidonState 0 0 0) lst); -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Data.Bool-src.html b/Stdlib.Data.Bool-src.html index 6eb9aeaa..52952efb 100644 --- a/Stdlib.Data.Bool-src.html +++ b/Stdlib.Data.Bool-src.html @@ -32,4 +32,4 @@ | true := "true" | false := "false" }; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Data.Bool.Base-src.html b/Stdlib.Data.Bool.Base-src.html index d166a8fb..126141f5 100644 --- a/Stdlib.Data.Bool.Base-src.html +++ b/Stdlib.Data.Bool.Base-src.html @@ -37,4 +37,4 @@ --- Logical conjunction. and (a b : Bool) : Bool := a && b; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Data.Field-src.html b/Stdlib.Data.Field-src.html index aedc3c42..b2f5b4fe 100644 --- a/Stdlib.Data.Field-src.html +++ b/Stdlib.Data.Field-src.html @@ -47,4 +47,4 @@ integralI := integralFieldI; / := (Field./) }; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Data.Field.Base-src.html b/Stdlib.Data.Field.Base-src.html index 65942741..d9f47fe3 100644 --- a/Stdlib.Data.Field.Base-src.html +++ b/Stdlib.Data.Field.Base-src.html @@ -43,4 +43,4 @@ fromNat (n : Nat) : Field := fromInt (ofNat n); toInt (f : Field) : Int := ofNat (toNat f); -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Data.Fixity-src.html b/Stdlib.Data.Fixity-src.html index 6798a45b..33ee8c41 100644 --- a/Stdlib.Data.Fixity-src.html +++ b/Stdlib.Data.Fixity-src.html @@ -2,4 +2,4 @@ 
module Stdlib.Data.Fixity;
 
 import Juvix.Builtin.V1.Fixity open public;
-
Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Data.Int-src.html b/Stdlib.Data.Int-src.html index e1950ad2..cfd17902 100644 --- a/Stdlib.Data.Int-src.html +++ b/Stdlib.Data.Int-src.html @@ -58,4 +58,4 @@ div := Int.div; mod := Int.mod }; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Data.Int.Base-src.html b/Stdlib.Data.Int.Base-src.html index f84d4b26..7fd96b8d 100644 --- a/Stdlib.Data.Int.Base-src.html +++ b/Stdlib.Data.Int.Base-src.html @@ -92,4 +92,4 @@ abs : Int -> Nat | (ofNat n) := n | (negSuc n) := suc n; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Data.Int.Ord-src.html b/Stdlib.Data.Int.Ord-src.html index 758bded2..caccc71b 100644 --- a/Stdlib.Data.Int.Ord-src.html +++ b/Stdlib.Data.Int.Ord-src.html @@ -59,4 +59,4 @@ --- Returns the biggest ;Int;. max (x y : Int) : Int := ite (x > y) x y; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Data.List-src.html b/Stdlib.Data.List-src.html index c581ab46..e60a1c1e 100644 --- a/Stdlib.Data.List-src.html +++ b/Stdlib.Data.List-src.html @@ -4,61 +4,73 @@ import Stdlib.Data.List.Base open public; import Stdlib.Data.Bool.Base open; import Stdlib.Data.String.Base open; +import Stdlib.Function open; import Stdlib.Trait.Eq open; import Stdlib.Trait.Ord open; import Stdlib.Trait.Show open; import Stdlib.Trait.Functor open; import Stdlib.Trait.Partial open; +import Stdlib.Trait.Foldable open using {Foldable; module Polymorphic; fromPolymorphicFoldable}; --- 𝒪(1). Partial function that returns the first element of a ;List;. -phead {A} {{Partial}} : List A -> A - | (x :: _) := x +phead {A} {{Partial}} : List A -> A + | (x :: _) := x | nil := fail "head: empty list"; instance -eqListI {A} {{Eq A}} : Eq (List A) := +eqListI {A} {{Eq A}} : Eq (List A) := let - go : List A -> List A -> Bool + go : List A -> List A -> Bool | nil nil := true | nil _ := false | _ nil := false - | (x :: xs) (y :: ys) := ite (Eq.eq x y) (go xs ys) false; - in mkEq go; + | (x :: xs) (y :: ys) := ite (Eq.eq x y) (go xs ys) false; + in mkEq go; instance -ordListI {A} {{Ord A}} : Ord (List A) := +ordListI {A} {{Ord A}} : Ord (List A) := let - go : List A -> List A -> Ordering + go : List A -> List A -> Ordering | nil nil := EQ | nil _ := LT | _ nil := GT - | (x :: xs) (y :: ys) := - case Ord.cmp x y of + | (x :: xs) (y :: ys) := + case Ord.cmp x y of | LT := LT | GT := GT - | EQ := go xs ys; - in mkOrd go; + | EQ := go xs ys; + in mkOrd go; instance -showListI {A} {{Show A}} : Show (List A) := +showListI {A} {{Show A}} : Show (List A) := let - go : List A -> String + go : List A -> String | nil := "nil" - | (x :: xs) := Show.show x ++str " :: " ++str go xs; + | (x :: xs) := Show.show x ++str " :: " ++str go xs; in mkShow λ { | nil := "nil" - | s := "(" ++str go s ++str ")" + | s := "(" ++str go s ++str ")" }; instance functorListI : Functor List := mkFunctor@{ - map := listMap + map := listMap }; instance -monomorphicFunctorListI {A} : Monomorphic.Functor (List A) A := +monomorphicFunctorListI {A} : Monomorphic.Functor (List A) A := fromPolymorphicFunctor; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file + +instance +polymorphicFoldableListI : Polymorphic.Foldable List := + Polymorphic.mkFoldable@{ + for := listFor; + rfor := listRfor + }; + +instance +foldableListI {A} : Foldable (List A) A := fromPolymorphicFoldable; +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Data.List.Base-src.html b/Stdlib.Data.List.Base-src.html index 553c2e95..7ecd9104 100644 --- a/Stdlib.Data.List.Base-src.html +++ b/Stdlib.Data.List.Base-src.html @@ -29,27 +29,27 @@ --- Right-associative fold. {-# specialize: [1] #-} -foldr {A B} (f : A → B → B) (z : B) : List A → B +liftFoldr {A B} (f : A → B → B) (z : B) : List A → B | nil := z - | (h :: hs) := f h (foldr f z hs); + | (h :: hs) := f h (liftFoldr f z hs); -syntax iterator rfor {init := 1; range := 1}; +syntax iterator listRfor {init := 1; range := 1}; {-# specialize: [1] #-} -rfor {A B} (f : B → A → B) (acc : B) : List A → B +listRfor {A B} (f : B → A → B) (acc : B) : List A → B | nil := acc - | (x :: xs) := f (rfor f acc xs) x; + | (x :: xs) := f (listRfor f acc xs) x; --- Left-associative and tail-recursive fold. {-# specialize: [1] #-} -foldl {A B} (f : B → A → B) (z : B) : List A → B +listFoldl {A B} (f : B → A → B) (z : B) : List A → B | nil := z - | (h :: hs) := foldl f (f z h) hs; + | (h :: hs) := listFoldl f (f z h) hs; -syntax iterator for {init := 1; range := 1}; +syntax iterator listFor {init := 1; range := 1}; {-# inline: 0, isabelle-function: {name: "foldl"} #-} -for : {A B : Type} → (B → A → B) → B → List A → B := foldl; +listFor : {A B : Type} → (B → A → B) → B → List A → B := listFoldl; syntax iterator listMap {init := 0; range := 1}; @@ -69,11 +69,11 @@ | (h :: hs) := ite (f h) (h :: filter f hs) (filter f hs); --- 𝒪(𝓃). Returns the length of the ;List;. -length {A} (l : List A) : Nat := for (acc := zero) (_ in l) {suc acc}; +length {A} (l : List A) : Nat := listFor (acc := zero) (_ in l) {suc acc}; --- 𝒪(𝓃). Returns the given ;List; in reverse order. {-# isabelle-function: {name: "rev"} #-} -reverse {A} (l : List A) : List A := for (acc := nil) (x in l) {x :: acc}; +reverse {A} (l : List A) : List A := listFor (acc := nil) (x in l) {x :: acc}; --- Returns a ;List; of length n where every element is the given value. replicate {A} : Nat → A → List A @@ -127,7 +127,7 @@ --- Concatenates a ;List; of ;List;s. {-# isabelle-function: {name: "concat"} #-} -flatten : {A : Type} → List (List A) → List A := foldl (++) nil; +flatten : {A : Type} → List (List A) → List A := listFoldl (++) nil; --- 𝒪(𝓃). Inserts the given element before every element in the given ;List;. prependToAll {A} (sep : A) : List A → List A @@ -231,4 +231,4 @@ | nil := nil | (xs :: nil) := listMap λ {x := x :: nil} xs | (xs :: xss) := zipWith (::) xs (transpose xss); -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Data.List.Base.html b/Stdlib.Data.List.Base.html index 061fc14d..0c8991dd 100644 --- a/Stdlib.Data.List.Base.html +++ b/Stdlib.Data.List.Base.html @@ -1,4 +1,4 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.List.Base

Definitions

import Juvix.Builtin.V1.List open public

elem {A} (eq : A → A → Bool) (s : A) : List A → BoolSource#

𝒪(𝓃). Returns true if the given object is in the List.

find {A} (predicate : A → Bool) : List A → Maybe ASource#

𝒪(𝓃). Returns the leftmost element of the list satisfying the predicate or nothing if there's no such element.

foldr {A B} (f : A → B → B) (z : B) : List A → BSource#

Right-associative fold.

rfor {A B} (f : B → A → B) (acc : B) : List A → BSource#

foldl {A B} (f : B → A → B) (z : B) : List A → BSource#

Left-associative and tail-recursive fold.

for : {A B : Type} → (B → A → B) → B → List A → BSource#

listMap {A B} (f : A → B) : List A → List BSource#

𝒪(𝓃). Maps a function over each element of a List.

filter {A} (f : A → Bool) : List A → List ASource#

𝒪(𝓃). Filters a List according to a given predicate, i.e., keeps the elements for which the given predicate returns true.

length {A} (l : List A) : NatSource#

𝒪(𝓃). Returns the length of the List.

reverse {A} (l : List A) : List ASource#

𝒪(𝓃). Returns the given List in reverse order.

replicate {A} : Nat → A → List ASource#

Returns a List of length n where every element is the given value.

take {A} : Nat → List A → List ASource#

Takes the first n elements of a List.

drop {A} : Nat → List A → List ASource#

Drops the first n elements of a List.

splitAt {A} : Nat → List A → Pair (List A) (List A)Source#

𝒪(𝓃). splitAt n xs returns a tuple where first element is xs prefix of length n and second element is the remainder of the List.

terminating +Juvix Documentation

stdlib - 0.0.1

Stdlib.Data.List.Base

Definitions

import Juvix.Builtin.V1.List open public

elem {A} (eq : A → A → Bool) (s : A) : List A → BoolSource#

𝒪(𝓃). Returns true if the given object is in the List.

find {A} (predicate : A → Bool) : List A → Maybe ASource#

𝒪(𝓃). Returns the leftmost element of the list satisfying the predicate or nothing if there's no such element.

liftFoldr {A B} (f : A → B → B) (z : B) : List A → BSource#

Right-associative fold.

listRfor {A B} (f : B → A → B) (acc : B) : List A → BSource#

listFoldl {A B} (f : B → A → B) (z : B) : List A → BSource#

Left-associative and tail-recursive fold.

listFor : {A B : Type} → (B → A → B) → B → List A → BSource#

listMap {A B} (f : A → B) : List A → List BSource#

𝒪(𝓃). Maps a function over each element of a List.

filter {A} (f : A → Bool) : List A → List ASource#

𝒪(𝓃). Filters a List according to a given predicate, i.e., keeps the elements for which the given predicate returns true.

length {A} (l : List A) : NatSource#

𝒪(𝓃). Returns the length of the List.

reverse {A} (l : List A) : List ASource#

𝒪(𝓃). Returns the given List in reverse order.

replicate {A} : Nat → A → List ASource#

Returns a List of length n where every element is the given value.

take {A} : Nat → List A → List ASource#

Takes the first n elements of a List.

drop {A} : Nat → List A → List ASource#

Drops the first n elements of a List.

splitAt {A} : Nat → List A → Pair (List A) (List A)Source#

𝒪(𝓃). splitAt n xs returns a tuple where first element is xs prefix of length n and second element is the remainder of the List.

terminating merge {A} {{Ord A}} : List A → List A → List ASource#

𝒪(𝓃 + 𝓂). Merges two lists according the given ordering.

partition {A} (f : A → Bool) : List A → Pair (List A) (List A)Source#

𝒪(𝓃). Returns a tuple where the first component has the items that satisfy the predicate and the second component has the elements that don't.

++ : {A : Type} → List A → List A → List ASource#

Concatenates two Lists.

snoc {A} (xs : List A) (x : A) : List ASource#

𝒪(𝓃). Append an element.

flatten : {A : Type} → List (List A) → List ASource#

Concatenates a List of Lists.

prependToAll {A} (sep : A) : List A → List ASource#

𝒪(𝓃). Inserts the given element before every element in the given List.

intersperse {A} (sep : A) : List A → List ASource#

𝒪(𝓃). Inserts the given element inbetween every two elements in the given List.

tail {A} : List A → List ASource#

𝒪(1). Drops the first element of a List.

head {A} (a : A) : List A -> ASource#

any {A} (f : A → Bool) : List A → BoolSource#

𝒪(𝓃). Returns true if at least one element of the List satisfies the predicate.

all {A} (f : A -> Bool) : List A -> BoolSource#

𝒪(𝓃). Returns true if all elements of the List satisfy the predicate.

null {A} : List A → BoolSource#

𝒪(1). Returns true if the List is empty.

zipWith {A B C} (f : A -> B -> C) : List A -> List B -> List CSource#

𝒪(min(𝓂, 𝓃)). Returns a list containing the results of applying a function to each pair of elements from the input lists.

zip {A B} : List A -> List B -> List (Pair A B)Source#

𝒪(min(𝓂, 𝓃)). Returns a list of pairs formed from the input lists.

mergeSort {A} {{Ord A}} (l : List A) : List ASource#

𝒪(𝓃 log 𝓃). Sorts a list of elements in ascending order using the MergeSort algorithm.

terminating quickSort {A} {{Ord A}} : List A → List ASource#

On average 𝒪(𝓃 log 𝓃), worst case 𝒪(𝓃²). Sorts a list of elements in ascending order using the QuickSort algorithm.

catMaybes {A} : List (Maybe A) -> List ASource#

𝒪(𝓃) Filters out every nothing from a List.

concatMap {A B} (f : A -> List B) : List A -> List BSource#

Applies a function to every item on a List and concatenates the result. 𝒪(𝓃), where 𝓃 is the number of items in the resulting list.

transpose {A} : List (List A) -> List (List A)Source#

𝒪(𝓃 * 𝓂). Transposes a List of Lists interpreted as a matrix.

\ No newline at end of file diff --git a/Stdlib.Data.List.html b/Stdlib.Data.List.html index 0fcb4200..b18f9b51 100644 --- a/Stdlib.Data.List.html +++ b/Stdlib.Data.List.html @@ -1,7 +1,9 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.List

Definitions

import Stdlib.Data.List.Base open public

phead {A} {{Partial}} : List A -> ASource#

𝒪(1). Partial function that returns the first element of a List.

instance -eqListI {A} {{Eq A}} : Eq (List A)Source#

instance -ordListI {A} {{Ord A}} : Ord (List A)Source#

instance -showListI {A} {{Show A}} : Show (List A)Source#

instance +Juvix Documentation

stdlib - 0.0.1

Stdlib.Data.List

Definitions

import Stdlib.Data.List.Base open public

phead {A} {{Partial}} : List A -> ASource#

𝒪(1). Partial function that returns the first element of a List.

instance +eqListI {A} {{Eq A}} : Eq (List A)Source#

instance +ordListI {A} {{Ord A}} : Ord (List A)Source#

instance +showListI {A} {{Show A}} : Show (List A)Source#

instance functorListI : Functor ListSource#

instance -monomorphicFunctorListI {A} : Monomorphic.Functor (List A) ASource#

\ No newline at end of file +monomorphicFunctorListI {A} : Monomorphic.Functor (List A) ASource#

instance +polymorphicFoldableListI : Polymorphic.Foldable ListSource#

instance +foldableListI {A} : Foldable (List A) ASource#

\ No newline at end of file diff --git a/Stdlib.Data.Maybe-src.html b/Stdlib.Data.Maybe-src.html index 5ead258d..6adf1a19 100644 --- a/Stdlib.Data.Maybe-src.html +++ b/Stdlib.Data.Maybe-src.html @@ -49,4 +49,4 @@ instance monomorphicFunctorMaybeI {A} : Monomorphic.Functor (Maybe A) A := fromPolymorphicFunctor; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Data.Maybe.Base-src.html b/Stdlib.Data.Maybe.Base-src.html index 535150b7..33ba7e84 100644 --- a/Stdlib.Data.Maybe.Base-src.html +++ b/Stdlib.Data.Maybe.Base-src.html @@ -15,4 +15,4 @@ maybe {A B} (b : B) (f : A → B) : Maybe A → B | nothing := b | (just a) := f a; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Data.Nat-src.html b/Stdlib.Data.Nat-src.html index f37a0144..d9c5d973 100644 --- a/Stdlib.Data.Nat-src.html +++ b/Stdlib.Data.Nat-src.html @@ -42,4 +42,4 @@ div := Nat.div; mod := Nat.mod }; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Data.Nat.Base-src.html b/Stdlib.Data.Nat.Base-src.html index 2a87314f..405849ff 100644 --- a/Stdlib.Data.Nat.Base-src.html +++ b/Stdlib.Data.Nat.Base-src.html @@ -2,4 +2,4 @@ 
module Stdlib.Data.Nat.Base;
 
 import Juvix.Builtin.V1.Nat.Base open public;
-
Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Data.Nat.Ord-src.html b/Stdlib.Data.Nat.Ord-src.html index 42bab68a..456266a8 100644 --- a/Stdlib.Data.Nat.Ord-src.html +++ b/Stdlib.Data.Nat.Ord-src.html @@ -60,4 +60,4 @@ --- Returns the larger ;Nat;. max (x y : Nat) : Nat := ite (x > y) x y; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Data.Pair-src.html b/Stdlib.Data.Pair-src.html index e24f7d7f..61d05d47 100644 --- a/Stdlib.Data.Pair-src.html +++ b/Stdlib.Data.Pair-src.html @@ -29,4 +29,4 @@ | {{mkShow show-a}} {{mkShow show-b}} := mkShow λ {(a, b) := "(" ++str show-a a ++str " , " ++str show-b b ++str ")"}; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Data.Pair.Base-src.html b/Stdlib.Data.Pair.Base-src.html index 522e1b54..6d877c72 100644 --- a/Stdlib.Data.Pair.Base-src.html +++ b/Stdlib.Data.Pair.Base-src.html @@ -39,4 +39,4 @@ --- Applies a function to both components. both {A B} (f : A → B) : Pair A A → Pair B B | (a, b) := f a, f b; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Data.Result-src.html b/Stdlib.Data.Result-src.html index bafbe4c8..68c74b70 100644 --- a/Stdlib.Data.Result-src.html +++ b/Stdlib.Data.Result-src.html @@ -37,4 +37,4 @@ monomorphicFunctorResultI {err res} : Monomorphic.Functor (Result err res) res := fromPolymorphicFunctor; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Data.Result.Base-src.html b/Stdlib.Data.Result.Base-src.html index 55007eac..010f0e95 100644 --- a/Stdlib.Data.Result.Base-src.html +++ b/Stdlib.Data.Result.Base-src.html @@ -53,4 +53,4 @@ maybeToResult {E A} (defaultError : E) : Maybe A -> Result E A | nothing := error defaultError | (just x) := ok x; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Data.String-src.html b/Stdlib.Data.String-src.html index b76942ba..6efac30d 100644 --- a/Stdlib.Data.String-src.html +++ b/Stdlib.Data.String-src.html @@ -16,4 +16,4 @@ let go (s : String) : String := "\"" ++str s ++str "\""; in mkShow go; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Data.String.Base-src.html b/Stdlib.Data.String.Base-src.html index b41245e1..34f4d0ce 100644 --- a/Stdlib.Data.String.Base-src.html +++ b/Stdlib.Data.String.Base-src.html @@ -7,8 +7,8 @@ import Stdlib.Data.Fixity open; --- Concatenates a ;List; of ;String;s. -concatStr : List String -> String := foldl (++str) ""; +concatStr : List String -> String := listFoldl (++str) ""; --- Joins a ;List; of ;String;s with "\n". unlines : List String -> String := intersperse "\n" >> concatStr; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Data.String.Ord-src.html b/Stdlib.Data.String.Ord-src.html index 16031c53..1022b10d 100644 --- a/Stdlib.Data.String.Ord-src.html +++ b/Stdlib.Data.String.Ord-src.html @@ -10,4 +10,4 @@ --- Equality for ;String;s. builtin string-eq axiom == : String → String → Bool; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Data.Unit-src.html b/Stdlib.Data.Unit-src.html index 92528eae..c2d78d0d 100644 --- a/Stdlib.Data.Unit-src.html +++ b/Stdlib.Data.Unit-src.html @@ -7,6 +7,7 @@ import Stdlib.Trait.Eq open; import Stdlib.Trait.Ord open; import Stdlib.Trait.Show open; +import Stdlib.Trait.Foldable open; type Unit := --- The only constructor of ;Unit;. @@ -20,4 +21,11 @@ instance showUnitI : Show Unit := mkShow λ {unit := "unit"}; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file + +instance +foldableUnitI : Foldable Unit Unit := + mkFoldable@{ + rfor {B : Type} (f : B -> Unit -> B) (ini : B) (_ : Unit) : B := f ini unit; + for {B : Type} (f : B -> Unit -> B) (ini : B) (_ : Unit) : B := f ini unit + }; +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Data.Unit.html b/Stdlib.Data.Unit.html index b21e773b..24bdc13d 100644 --- a/Stdlib.Data.Unit.html +++ b/Stdlib.Data.Unit.html @@ -2,4 +2,5 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Unit

Description

The unit type.

Definitions

type UnitSource#

Constructors

| unit

The only constructor of Unit.

instance eqUnitI : Eq UnitSource#

instance ordUnitI : Ord UnitSource#

instance -showUnitI : Show UnitSource#

\ No newline at end of file +showUnitI : Show UnitSource#

instance +foldableUnitI : Foldable Unit UnitSource#

\ No newline at end of file diff --git a/Stdlib.Debug.Fail-src.html b/Stdlib.Debug.Fail-src.html index 24c9257c..e66f15e9 100644 --- a/Stdlib.Debug.Fail-src.html +++ b/Stdlib.Debug.Fail-src.html @@ -6,4 +6,4 @@ --- Primitive that exits the program with an error message. builtin fail axiom failwith : {A : Type} → String → A; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Function-src.html b/Stdlib.Function-src.html index 460bf6a5..a163fcfb 100644 --- a/Stdlib.Function-src.html +++ b/Stdlib.Function-src.html @@ -55,4 +55,4 @@ builtin seq >-> : {A B : Type} → A → B → B | x y := y; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Prelude-src.html b/Stdlib.Prelude-src.html index 8b182a94..33359665 100644 --- a/Stdlib.Prelude-src.html +++ b/Stdlib.Prelude-src.html @@ -18,4 +18,4 @@ import Stdlib.System.IO open public; import Stdlib.Trait open public; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.System.IO-src.html b/Stdlib.System.IO-src.html index ca7c42a6..db002c8f 100644 --- a/Stdlib.System.IO-src.html +++ b/Stdlib.System.IO-src.html @@ -12,4 +12,4 @@ print {A} {{Show A}} (a : A) : IO := printString (Show.show a); printLn {A} {{Show A}} (a : A) : IO := printStringLn (Show.show a); -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.System.IO.Base-src.html b/Stdlib.System.IO.Base-src.html index 1bdac099..6946e3a5 100644 --- a/Stdlib.System.IO.Base-src.html +++ b/Stdlib.System.IO.Base-src.html @@ -9,4 +9,4 @@ syntax operator >>> seq; builtin IO-sequence axiom >>> : IO → IO → IO; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.System.IO.Bool-src.html b/Stdlib.System.IO.Bool-src.html index 5bbdea0a..82659087 100644 --- a/Stdlib.System.IO.Bool-src.html +++ b/Stdlib.System.IO.Bool-src.html @@ -9,4 +9,4 @@ axiom printBool : Bool → IO; printBoolLn (b : Bool) : IO := printBool b >>> printString "\n"; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.System.IO.Int-src.html b/Stdlib.System.IO.Int-src.html index a0c33aef..029069f9 100644 --- a/Stdlib.System.IO.Int-src.html +++ b/Stdlib.System.IO.Int-src.html @@ -9,4 +9,4 @@ axiom printInt : Int → IO; printIntLn (i : Int) : IO := printInt i >>> printString "\n"; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.System.IO.Nat-src.html b/Stdlib.System.IO.Nat-src.html index 5baced14..04a9895e 100644 --- a/Stdlib.System.IO.Nat-src.html +++ b/Stdlib.System.IO.Nat-src.html @@ -9,4 +9,4 @@ axiom printNat : Nat → IO; printNatLn (n : Nat) : IO := printNat n >>> printString "\n"; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.System.IO.String-src.html b/Stdlib.System.IO.String-src.html index e49abff6..b81c8c7c 100644 --- a/Stdlib.System.IO.String-src.html +++ b/Stdlib.System.IO.String-src.html @@ -11,4 +11,4 @@ axiom readLn : (String → IO) → IO; printStringLn (s : String) : IO := printString s >>> printString "\n"; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Trait-src.html b/Stdlib.Trait-src.html index 3fcbed8a..f99cbe2a 100644 --- a/Stdlib.Trait-src.html +++ b/Stdlib.Trait-src.html @@ -5,9 +5,10 @@ import Stdlib.Trait.Show as Show open using {Show; module Show} public; import Stdlib.Trait.Ord as Ord open using {Ord; module Ord} public; import Stdlib.Trait.Functor open public; +import Stdlib.Trait.Foldable open public; import Stdlib.Trait.Partial open public; import Stdlib.Trait.Natural open public; import Stdlib.Trait.Integral open public; import Stdlib.Trait.Numeric open public; import Stdlib.Trait.DivMod open public; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Trait.DivMod-src.html b/Stdlib.Trait.DivMod-src.html index 1c4b9b3c..3c4a0bb9 100644 --- a/Stdlib.Trait.DivMod-src.html +++ b/Stdlib.Trait.DivMod-src.html @@ -11,4 +11,4 @@ }; open DivMod public; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Eq-src.html b/Stdlib.Trait.Eq-src.html index 87a30ab7..9485feac 100644 --- a/Stdlib.Trait.Eq-src.html +++ b/Stdlib.Trait.Eq-src.html @@ -17,4 +17,4 @@ --- Tests for inequality. {-# inline: always, isabelle-operator: {name: "≠", prec: 50, assoc: none} #-} /= {A} {{Eq A}} (x y : A) : Bool := not (x == y); -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Foldable-src.html b/Stdlib.Trait.Foldable-src.html new file mode 100644 index 00000000..e9f97090 --- /dev/null +++ b/Stdlib.Trait.Foldable-src.html @@ -0,0 +1,6 @@ + +
module Stdlib.Trait.Foldable;
+
+import Stdlib.Trait.Foldable.Polymorphic as Polymorphic public;
+import Stdlib.Trait.Foldable.Monomorphic open public;
+
Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Foldable.Monomorphic-src.html b/Stdlib.Trait.Foldable.Monomorphic-src.html new file mode 100644 index 00000000..8f9c7ae5 --- /dev/null +++ b/Stdlib.Trait.Foldable.Monomorphic-src.html @@ -0,0 +1,50 @@ + +
module Stdlib.Trait.Foldable.Monomorphic;
+
+import Stdlib.Function open;
+import Stdlib.Trait.Foldable.Polymorphic as Poly;
+
+--- A trait for combining elements into a single result, processing one element at a time.
+trait
+type Foldable (container elem : Type) :=
+  mkFoldable {
+    syntax iterator for {init := 1; range := 1};
+    {-# inline: 0 #-}
+    for : {B : Type} -> (B -> elem -> B) -> B -> container -> B;
+
+    syntax iterator rfor {init := 1; range := 1};
+    {-# inline: 0 #-}
+    rfor : {B : Type} -> (B -> elem -> B) -> B → container → B
+  };
+
+open Foldable;
+
+--- Make a monomorphic ;Foldable; instance from a polymorphic one.
+--- All polymorphic types that are an instance of ;Poly.Foldable; should use this function to create their monomorphic ;Foldable; instance.
+fromPolymorphicFoldable
+  {f : Type -> Type}
+  {{foldable : Poly.Foldable f}}
+  {elem}
+  : Foldable (f elem) elem :=
+  mkFoldable@{
+    for := Poly.for;
+    rfor := Poly.rfor
+  };
+
+foldl
+  {container elem}
+  {{Foldable container elem}}
+  {B : Type}
+  (g : B -> elem -> B)
+  (ini : B)
+  (ls : container)
+  : B := for (acc := ini) (x in ls) {g acc x};
+
+--- Combine the elements of the type using the provided function starting with the element in the right-most position.
+foldr
+  {container elem : Type}
+  {{Foldable container elem}}
+  {B : Type}
+  (g : elem -> B -> B)
+  : B -> container -> B := foldl (flip g);
+
Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Foldable.Monomorphic.html b/Stdlib.Trait.Foldable.Monomorphic.html new file mode 100644 index 00000000..242c060a --- /dev/null +++ b/Stdlib.Trait.Foldable.Monomorphic.html @@ -0,0 +1,26 @@ + +Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Foldable.Monomorphic

Definitions

trait +type Foldable (container elem : Type)Source#

A trait for combining elements into a single result, processing one element at a time.

Constructors

| mkFoldable { + syntax iterator for {init := 1; range := 1}; + {-# inline: 0 #-} + for : {B : Type} -> (B -> elem -> B) -> B -> container -> B; + syntax iterator rfor {init := 1; range := 1}; + {-# inline: 0 #-} + rfor : {B : Type} -> (B -> elem -> B) -> B → container → B + }

fromPolymorphicFoldable + {f : Type -> Type} + {{foldable : Poly.Foldable f}} + {elem} + : Foldable (f elem) elemSource#

Make a monomorphic Foldable instance from a polymorphic one. All polymorphic types that are an instance of Poly.Foldable should use this function to create their monomorphic Foldable instance.

foldl + {container elem} + {{Foldable container elem}} + {B : Type} + (g : B -> elem -> B) + (ini : B) + (ls : container) + : BSource#

foldr + {container elem : Type} + {{Foldable container elem}} + {B : Type} + (g : elem -> B -> B) + : B -> container -> BSource#

Combine the elements of the type using the provided function starting with the element in the right-most position.

\ No newline at end of file diff --git a/Stdlib.Trait.Foldable.Polymorphic-src.html b/Stdlib.Trait.Foldable.Polymorphic-src.html new file mode 100644 index 00000000..a622a647 --- /dev/null +++ b/Stdlib.Trait.Foldable.Polymorphic-src.html @@ -0,0 +1,40 @@ + +
module Stdlib.Trait.Foldable.Polymorphic;
+
+import Stdlib.Function open;
+
+--- A trait for combining elements into a single result, processing one element at a time.
+trait
+type Foldable (f : Type -> Type) :=
+  mkFoldable {
+    syntax iterator for {init := 1; range := 1};
+    {-# inline: 0 #-}
+    for : {A B : Type} -> (B -> A -> B) -> B -> f A -> B;
+
+    syntax iterator rfor {init := 1; range := 1};
+    {-# inline: 0 #-}
+    rfor : {A B : Type} -> (B → A → B) -> B → f A → B
+  };
+
+open Foldable public;
+
+--- Combine the elements of the type using the provided function starting with the element in the left-most position.
+foldl
+  {f : Type -> Type}
+  {{Foldable f}}
+  {A B : Type}
+  (g : B -> A -> B)
+  (ini : B)
+  (ls : f A)
+  : B := for (acc := ini) (x in ls) {g acc x};
+
+--- Combine the elements of the type using the provided function starting with the element in the right-most position.
+foldr
+  {f : Type -> Type}
+  {{Foldable f}}
+  {A B : Type}
+  (g : A -> B -> B)
+  (ini : B)
+  (ls : f A)
+  : B := rfor (acc := ini) (x in ls) {g x acc};
+
Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Foldable.Polymorphic.html b/Stdlib.Trait.Foldable.Polymorphic.html new file mode 100644 index 00000000..a71c71f8 --- /dev/null +++ b/Stdlib.Trait.Foldable.Polymorphic.html @@ -0,0 +1,24 @@ + +Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Foldable.Polymorphic

Definitions

trait +type Foldable (f : Type -> Type)Source#

A trait for combining elements into a single result, processing one element at a time.

Constructors

| mkFoldable { + syntax iterator for {init := 1; range := 1}; + {-# inline: 0 #-} + for : {A B : Type} -> (B -> A -> B) -> B -> f A -> B; + syntax iterator rfor {init := 1; range := 1}; + {-# inline: 0 #-} + rfor : {A B : Type} -> (B → A → B) -> B → f A → B + }

open Foldable public

foldl + {f : Type -> Type} + {{Foldable f}} + {A B : Type} + (g : B -> A -> B) + (ini : B) + (ls : f A) + : BSource#

Combine the elements of the type using the provided function starting with the element in the left-most position.

foldr + {f : Type -> Type} + {{Foldable f}} + {A B : Type} + (g : A -> B -> B) + (ini : B) + (ls : f A) + : BSource#

Combine the elements of the type using the provided function starting with the element in the right-most position.

\ No newline at end of file diff --git a/Stdlib.Trait.Foldable.html b/Stdlib.Trait.Foldable.html new file mode 100644 index 00000000..e0a55ea2 --- /dev/null +++ b/Stdlib.Trait.Foldable.html @@ -0,0 +1,2 @@ + +Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Foldable

\ No newline at end of file diff --git a/Stdlib.Trait.Functor-src.html b/Stdlib.Trait.Functor-src.html index 8feae764..db99df02 100644 --- a/Stdlib.Trait.Functor-src.html +++ b/Stdlib.Trait.Functor-src.html @@ -4,4 +4,4 @@ import Stdlib.Trait.Functor.Polymorphic open public; import Stdlib.Trait.Functor.Monomorphic as Monomorphic public; import Stdlib.Trait.Functor.Monomorphic open using {fromPolymorphicFunctor} public; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Functor.Monomorphic-src.html b/Stdlib.Trait.Functor.Monomorphic-src.html index 67dbd665..33cac7d1 100644 --- a/Stdlib.Trait.Functor.Monomorphic-src.html +++ b/Stdlib.Trait.Functor.Monomorphic-src.html @@ -33,4 +33,4 @@ (fa : container) (b : elem) : container := λ {_ := b} <$> fa; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Functor.Polymorphic-src.html b/Stdlib.Trait.Functor.Polymorphic-src.html index d339607e..cd5f3539 100644 --- a/Stdlib.Trait.Functor.Polymorphic-src.html +++ b/Stdlib.Trait.Functor.Polymorphic-src.html @@ -22,4 +22,4 @@ void {f : Type → Type} {A : Type} {{Functor f}} (fa : f A) : f Unit := fa $> unit; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Integral-src.html b/Stdlib.Trait.Integral-src.html index d088d81e..4cea0b89 100644 --- a/Stdlib.Trait.Integral-src.html +++ b/Stdlib.Trait.Integral-src.html @@ -17,4 +17,4 @@ }; open Integral using {fromInt; -} public; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Natural-src.html b/Stdlib.Trait.Natural-src.html index 4883a2d5..6339fc0d 100644 --- a/Stdlib.Trait.Natural-src.html +++ b/Stdlib.Trait.Natural-src.html @@ -2,4 +2,4 @@ 
module Stdlib.Trait.Natural;
 
 import Juvix.Builtin.V1.Trait.Natural open public;
-
Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Numeric-src.html b/Stdlib.Trait.Numeric-src.html index 348d69e2..ee72d47c 100644 --- a/Stdlib.Trait.Numeric-src.html +++ b/Stdlib.Trait.Numeric-src.html @@ -13,4 +13,4 @@ }; open Numeric using {/} public; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Ord-src.html b/Stdlib.Trait.Ord-src.html index ac9e1f32..52337086 100644 --- a/Stdlib.Trait.Ord-src.html +++ b/Stdlib.Trait.Ord-src.html @@ -74,4 +74,4 @@ --- Returns the larger element. {-# inline: always #-} max {A} {{Ord A}} (x y : A) : A := ite (x > y) x y; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Partial-src.html b/Stdlib.Trait.Partial-src.html index 5558ea88..67d91b9c 100644 --- a/Stdlib.Trait.Partial-src.html +++ b/Stdlib.Trait.Partial-src.html @@ -10,4 +10,4 @@ open Partial public; runPartial {A} (f : {{Partial}} -> A) : A := f {{mkPartial Debug.failwith}}; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Show-src.html b/Stdlib.Trait.Show-src.html index 365f4d73..eb5345ba 100644 --- a/Stdlib.Trait.Show-src.html +++ b/Stdlib.Trait.Show-src.html @@ -5,4 +5,4 @@ trait type Show A := mkShow {show : A -> String}; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/Stdlib.Trait.html b/Stdlib.Trait.html index cd449301..1eb56141 100644 --- a/Stdlib.Trait.html +++ b/Stdlib.Trait.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait

Definitions

import Stdlib.Trait.Eq as Eq open using {Eq; module Eq} public

import Stdlib.Trait.Show as Show open using {Show; module Show} public

import Stdlib.Trait.Ord as Ord open using {Ord; module Ord} public

import Stdlib.Trait.Functor open public

import Stdlib.Trait.Partial open public

import Stdlib.Trait.Natural open public

import Stdlib.Trait.Integral open public

import Stdlib.Trait.Numeric open public

import Stdlib.Trait.DivMod open public

\ No newline at end of file +Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait

Definitions

import Stdlib.Trait.Eq as Eq open using {Eq; module Eq} public

import Stdlib.Trait.Show as Show open using {Show; module Show} public

import Stdlib.Trait.Ord as Ord open using {Ord; module Ord} public

import Stdlib.Trait.Functor open public

import Stdlib.Trait.Foldable open public

import Stdlib.Trait.Partial open public

import Stdlib.Trait.Natural open public

import Stdlib.Trait.Integral open public

import Stdlib.Trait.Numeric open public

import Stdlib.Trait.DivMod open public

\ No newline at end of file diff --git a/index-src.html b/index-src.html index 40314d43..76c64c05 100644 --- a/index-src.html +++ b/index-src.html @@ -16,4 +16,4 @@ import Stdlib.Data.String.Ord; import Stdlib.Cairo.Poseidon; -Last modified on 2024-07-23 11:12 UTC \ No newline at end of file +Last modified on 2024-07-23 15:18 UTC \ No newline at end of file diff --git a/index.html b/index.html index 7d3f080d..78068935 100644 --- a/index.html +++ b/index.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1
\ No newline at end of file +Juvix Documentation
stdlib - 0.0.1
\ No newline at end of file