From 3180dbb6929f44bfb58136457d326a4acf768d7d Mon Sep 17 00:00:00 2001 From: paulcadman Date: Mon, 25 Nov 2024 03:42:46 +0000 Subject: [PATCH] deploy: b50851a41eddf0b77a82a62251dc4ce9a3c4d57a --- Juvix.Builtin.V1.Bool-src.html | 4 +- Juvix.Builtin.V1.Bool.html | 4 +- Juvix.Builtin.V1.Fixity-src.html | 4 +- Juvix.Builtin.V1.Fixity.html | 2 +- Juvix.Builtin.V1.List-src.html | 4 +- Juvix.Builtin.V1.List.html | 4 +- Juvix.Builtin.V1.Maybe-src.html | 4 +- Juvix.Builtin.V1.Maybe.html | 4 +- Juvix.Builtin.V1.Nat-src.html | 4 +- Juvix.Builtin.V1.Nat.Base-src.html | 4 +- Juvix.Builtin.V1.Nat.Base.html | 4 +- Juvix.Builtin.V1.Nat.html | 4 +- Juvix.Builtin.V1.String-src.html | 4 +- Juvix.Builtin.V1.String.html | 4 +- Juvix.Builtin.V1.Trait.FromNatural-src.html | 4 +- Juvix.Builtin.V1.Trait.FromNatural.html | 4 +- Juvix.Builtin.V1.Trait.Natural-src.html | 4 +- Juvix.Builtin.V1.Trait.Natural.html | 4 +- Stdlib.Cairo.Ec-src.html | 4 +- Stdlib.Cairo.Ec.html | 4 +- Stdlib.Cairo.Pedersen-src.html | 4 +- Stdlib.Cairo.Pedersen.html | 2 +- Stdlib.Cairo.Poseidon-src.html | 4 +- Stdlib.Cairo.Poseidon.html | 4 +- Stdlib.Data.BinaryTree-src.html | 4 +- Stdlib.Data.BinaryTree.html | 4 +- Stdlib.Data.Bool-src.html | 4 +- Stdlib.Data.Bool.Base-src.html | 4 +- Stdlib.Data.Bool.Base.html | 4 +- Stdlib.Data.Bool.html | 4 +- Stdlib.Data.Byte-src.html | 4 +- Stdlib.Data.Byte.Base-src.html | 4 +- Stdlib.Data.Byte.Base.html | 4 +- Stdlib.Data.Byte.html | 4 +- Stdlib.Data.Field-src.html | 4 +- Stdlib.Data.Field.Base-src.html | 4 +- Stdlib.Data.Field.Base.html | 4 +- Stdlib.Data.Field.html | 4 +- Stdlib.Data.Fixity-src.html | 4 +- Stdlib.Data.Fixity.html | 2 +- Stdlib.Data.Int-src.html | 4 +- Stdlib.Data.Int.Base-src.html | 4 +- Stdlib.Data.Int.Base.html | 4 +- Stdlib.Data.Int.Ord-src.html | 4 +- Stdlib.Data.Int.Ord.html | 4 +- Stdlib.Data.Int.html | 4 +- Stdlib.Data.List-src.html | 12 ++-- Stdlib.Data.List.Base-src.html | 4 +- Stdlib.Data.List.Base.html | 4 +- Stdlib.Data.List.html | 4 +- Stdlib.Data.Map-src.html | 28 ++++---- Stdlib.Data.Map.html | 4 +- Stdlib.Data.Maybe-src.html | 4 +- Stdlib.Data.Maybe.Base-src.html | 4 +- Stdlib.Data.Maybe.Base.html | 2 +- Stdlib.Data.Maybe.html | 4 +- Stdlib.Data.Nat-src.html | 4 +- Stdlib.Data.Nat.Base-src.html | 4 +- Stdlib.Data.Nat.Base.html | 2 +- Stdlib.Data.Nat.Ord-src.html | 4 +- Stdlib.Data.Nat.Ord.html | 4 +- Stdlib.Data.Nat.html | 4 +- Stdlib.Data.Pair-src.html | 4 +- Stdlib.Data.Pair.Base-src.html | 4 +- Stdlib.Data.Pair.Base.html | 4 +- Stdlib.Data.Pair.html | 4 +- Stdlib.Data.Queue-src.html | 4 +- Stdlib.Data.Queue.Base-src.html | 6 +- Stdlib.Data.Queue.Base.html | 4 +- Stdlib.Data.Queue.html | 2 +- Stdlib.Data.Range-src.html | 4 +- Stdlib.Data.Range.html | 4 +- Stdlib.Data.Result-src.html | 4 +- Stdlib.Data.Result.Base-src.html | 4 +- Stdlib.Data.Result.Base.html | 4 +- Stdlib.Data.Result.html | 4 +- Stdlib.Data.Set-src.html | 4 +- Stdlib.Data.Set.AVL-src.html | 30 ++++----- Stdlib.Data.Set.AVL.html | 4 +- Stdlib.Data.Set.html | 2 +- Stdlib.Data.String-src.html | 4 +- Stdlib.Data.String.Base-src.html | 4 +- Stdlib.Data.String.Base.html | 2 +- Stdlib.Data.String.Ord-src.html | 4 +- Stdlib.Data.String.Ord.html | 4 +- Stdlib.Data.String.html | 4 +- Stdlib.Data.Tree-src.html | 4 +- Stdlib.Data.Tree.html | 4 +- Stdlib.Data.UnbalancedSet-src.html | 4 +- Stdlib.Data.UnbalancedSet.html | 4 +- Stdlib.Data.Unit-src.html | 4 +- Stdlib.Data.Unit.Base-src.html | 4 +- Stdlib.Data.Unit.Base.html | 2 +- Stdlib.Data.Unit.html | 4 +- Stdlib.Debug-src.html | 4 +- Stdlib.Debug.Fail-src.html | 4 +- Stdlib.Debug.Fail.html | 4 +- Stdlib.Debug.Trace-src.html | 4 +- Stdlib.Debug.Trace.html | 4 +- Stdlib.Debug.html | 2 +- Stdlib.Extra.Gcd-src.html | 4 +- Stdlib.Extra.Gcd.html | 2 +- Stdlib.Function-src.html | 4 +- Stdlib.Function.html | 4 +- Stdlib.Prelude-src.html | 4 +- Stdlib.Prelude.html | 2 +- Stdlib.System.IO-src.html | 4 +- Stdlib.System.IO.Base-src.html | 4 +- Stdlib.System.IO.Base.html | 4 +- Stdlib.System.IO.Bool-src.html | 4 +- Stdlib.System.IO.Bool.html | 4 +- Stdlib.System.IO.Int-src.html | 4 +- Stdlib.System.IO.Int.html | 4 +- Stdlib.System.IO.Nat-src.html | 4 +- Stdlib.System.IO.Nat.html | 4 +- Stdlib.System.IO.String-src.html | 4 +- Stdlib.System.IO.String.html | 4 +- Stdlib.System.IO.html | 2 +- Stdlib.Trait-src.html | 4 +- Stdlib.Trait.Applicative-src.html | 74 ++++++++++----------- Stdlib.Trait.Applicative.html | 36 +++++----- Stdlib.Trait.DivMod-src.html | 4 +- Stdlib.Trait.DivMod.html | 4 +- Stdlib.Trait.Eq-src.html | 4 +- Stdlib.Trait.Eq.html | 4 +- Stdlib.Trait.Foldable-src.html | 4 +- Stdlib.Trait.Foldable.Monomorphic-src.html | 60 ++++++++--------- Stdlib.Trait.Foldable.Monomorphic.html | 44 ++++++------ Stdlib.Trait.Foldable.Polymorphic-src.html | 50 +++++++------- Stdlib.Trait.Foldable.Polymorphic.html | 36 +++++----- Stdlib.Trait.Foldable.html | 2 +- Stdlib.Trait.FromNatural-src.html | 4 +- Stdlib.Trait.FromNatural.html | 2 +- Stdlib.Trait.Functor-src.html | 4 +- Stdlib.Trait.Functor.Monomorphic-src.html | 6 +- Stdlib.Trait.Functor.Monomorphic.html | 4 +- Stdlib.Trait.Functor.Polymorphic-src.html | 20 +++--- Stdlib.Trait.Functor.Polymorphic.html | 6 +- Stdlib.Trait.Functor.html | 4 +- Stdlib.Trait.Integral-src.html | 4 +- Stdlib.Trait.Integral.html | 4 +- Stdlib.Trait.Monad-src.html | 28 ++++---- Stdlib.Trait.Monad.html | 20 +++--- Stdlib.Trait.Natural-src.html | 4 +- Stdlib.Trait.Natural.html | 2 +- Stdlib.Trait.Numeric-src.html | 4 +- Stdlib.Trait.Numeric.html | 4 +- Stdlib.Trait.Ord-src.html | 4 +- Stdlib.Trait.Ord.html | 4 +- Stdlib.Trait.Partial-src.html | 12 ++-- Stdlib.Trait.Partial.html | 4 +- Stdlib.Trait.Show-src.html | 4 +- Stdlib.Trait.Show.html | 4 +- Stdlib.Trait.html | 2 +- assets/css/latte-light.css | 30 +++++++++ index-src.html | 4 +- index.html | 2 +- 157 files changed, 526 insertions(+), 496 deletions(-) create mode 100644 assets/css/latte-light.css diff --git a/Juvix.Builtin.V1.Bool-src.html b/Juvix.Builtin.V1.Bool-src.html index e830be25..24815d40 100644 --- a/Juvix.Builtin.V1.Bool-src.html +++ b/Juvix.Builtin.V1.Bool-src.html @@ -1,9 +1,9 @@ -
module Juvix.Builtin.V1.Bool;
+
module Juvix.Builtin.V1.Bool;
 
 --- Inductive definition of booleans.
 builtin bool
 type Bool :=
   | true
   | false;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
\ No newline at end of file diff --git a/Juvix.Builtin.V1.Bool.html b/Juvix.Builtin.V1.Bool.html index 7b1956aa..93b13ba7 100644 --- a/Juvix.Builtin.V1.Bool.html +++ b/Juvix.Builtin.V1.Bool.html @@ -1,3 +1,3 @@ -Juvix Documentation
stdlib - 0.0.1

Juvix.Builtin.V1.Bool

Definitions

builtin bool -type BoolSource#

Inductive definition of booleans.

Constructors

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

Juvix.Builtin.V1.Bool

Definitions

builtin bool +type BoolSource#

Inductive definition of booleans.

Constructors

| true
| false
\ No newline at end of file diff --git a/Juvix.Builtin.V1.Fixity-src.html b/Juvix.Builtin.V1.Fixity-src.html index 962e4742..176296a2 100644 --- a/Juvix.Builtin.V1.Fixity-src.html +++ b/Juvix.Builtin.V1.Fixity-src.html @@ -1,5 +1,5 @@ -
module Juvix.Builtin.V1.Fixity;
+
module Juvix.Builtin.V1.Fixity;
 
 syntax fixity none := none;
 
@@ -26,4 +26,4 @@
 
 syntax fixity composition := binary {assoc := right; above := [multiplicative]};
 syntax fixity lcomposition := binary {assoc := left; above := [multiplicative]};
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
\ No newline at end of file diff --git a/Juvix.Builtin.V1.Fixity.html b/Juvix.Builtin.V1.Fixity.html index 4274eba0..f3e023e1 100644 --- a/Juvix.Builtin.V1.Fixity.html +++ b/Juvix.Builtin.V1.Fixity.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Juvix.Builtin.V1.Fixity

Definitions

syntax fixity noneSource#

Fixity details

none

syntax fixity rappSource#

Fixity details

binary; right-associative

syntax fixity lappSource#

Fixity details

binary; left-associative
Same precedence as rapp

syntax fixity seqSource#

Fixity details

binary; left-associative
Higher precedence than: lapp

syntax fixity functorSource#

Fixity details

binary; right-associative

syntax fixity logicalSource#

Fixity details

binary; right-associative
Higher precedence than: seq

syntax fixity comparisonSource#

Fixity details

binary
Higher precedence than: logical

syntax fixity pairSource#

Fixity details

binary; right-associative

syntax fixity consSource#

Fixity details

binary; right-associative
Higher precedence than: pair

syntax fixity stepSource#

Fixity details

binary; right-associative

syntax fixity rangeSource#

Fixity details

binary; right-associative
Higher precedence than: step

syntax fixity additiveSource#

Fixity details

binary; left-associative
Higher precedence than: comparison; range; cons

syntax fixity multiplicativeSource#

Fixity details

binary; left-associative
Higher precedence than: additive

syntax fixity compositionSource#

Fixity details

binary; right-associative
Higher precedence than: multiplicative

syntax fixity lcompositionSource#

Fixity details

binary; left-associative
Higher precedence than: multiplicative
\ No newline at end of file +Juvix Documentation
stdlib - 0.0.1

Juvix.Builtin.V1.Fixity

Definitions

syntax fixity noneSource#

Fixity details

none

syntax fixity rappSource#

Fixity details

binary; right-associative

syntax fixity lappSource#

Fixity details

binary; left-associative
Same precedence as rapp

syntax fixity seqSource#

Fixity details

binary; left-associative
Higher precedence than: lapp

syntax fixity functorSource#

Fixity details

binary; right-associative

syntax fixity logicalSource#

Fixity details

binary; right-associative
Higher precedence than: seq

syntax fixity comparisonSource#

Fixity details

binary
Higher precedence than: logical

syntax fixity pairSource#

Fixity details

binary; right-associative

syntax fixity consSource#

Fixity details

binary; right-associative
Higher precedence than: pair

syntax fixity stepSource#

Fixity details

binary; right-associative

syntax fixity rangeSource#

Fixity details

binary; right-associative
Higher precedence than: step

syntax fixity additiveSource#

Fixity details

binary; left-associative
Higher precedence than: comparison; range; cons

syntax fixity multiplicativeSource#

Fixity details

binary; left-associative
Higher precedence than: additive

syntax fixity compositionSource#

Fixity details

binary; right-associative
Higher precedence than: multiplicative

syntax fixity lcompositionSource#

Fixity details

binary; left-associative
Higher precedence than: multiplicative
\ No newline at end of file diff --git a/Juvix.Builtin.V1.List-src.html b/Juvix.Builtin.V1.List-src.html index 82816aac..7bc0cf8e 100644 --- a/Juvix.Builtin.V1.List-src.html +++ b/Juvix.Builtin.V1.List-src.html @@ -1,5 +1,5 @@ -
module Juvix.Builtin.V1.List;
+
module Juvix.Builtin.V1.List;
 
 import Juvix.Builtin.V1.Fixity open;
 
@@ -11,4 +11,4 @@
     nil
   | --- An element followed by a list
     :: A (List A);
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
\ No newline at end of file diff --git a/Juvix.Builtin.V1.List.html b/Juvix.Builtin.V1.List.html index 27d4933d..35dcee34 100644 --- a/Juvix.Builtin.V1.List.html +++ b/Juvix.Builtin.V1.List.html @@ -1,3 +1,3 @@ -Juvix Documentation
stdlib - 0.0.1

Juvix.Builtin.V1.List

Definitions

builtin list -type List (A : Type)Source#

Inductive list.

Constructors

| nil

The empty list

| :: A (List A)

An element followed by a list

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

Juvix.Builtin.V1.List

Definitions

builtin list +type List (A : Type)Source#

Inductive list.

Constructors

| nil

The empty list

| :: A (List A)

An element followed by a list

\ No newline at end of file diff --git a/Juvix.Builtin.V1.Maybe-src.html b/Juvix.Builtin.V1.Maybe-src.html index b22ef461..5fe1af5f 100644 --- a/Juvix.Builtin.V1.Maybe-src.html +++ b/Juvix.Builtin.V1.Maybe-src.html @@ -1,5 +1,5 @@ -
module Juvix.Builtin.V1.Maybe;
+
module Juvix.Builtin.V1.Maybe;
 
 --- Represents an optional value that may or may not be present. Provides a way
 --- to handle null or missing values in a type-safe manner.
@@ -7,4 +7,4 @@
 type Maybe A :=
   | nothing
   | just A;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
\ No newline at end of file diff --git a/Juvix.Builtin.V1.Maybe.html b/Juvix.Builtin.V1.Maybe.html index 155b52dc..ce911b45 100644 --- a/Juvix.Builtin.V1.Maybe.html +++ b/Juvix.Builtin.V1.Maybe.html @@ -1,3 +1,3 @@ -Juvix Documentation
stdlib - 0.0.1

Juvix.Builtin.V1.Maybe

Definitions

builtin maybe -type Maybe ASource#

Represents an optional value that may or may not be present. Provides a way to handle null or missing values in a type-safe manner.

Constructors

| nothing
| just A
\ No newline at end of file +Juvix Documentation
stdlib - 0.0.1

Juvix.Builtin.V1.Maybe

Definitions

builtin maybe +type Maybe ASource#

Represents an optional value that may or may not be present. Provides a way to handle null or missing values in a type-safe manner.

Constructors

| nothing
| just A
\ No newline at end of file diff --git a/Juvix.Builtin.V1.Nat-src.html b/Juvix.Builtin.V1.Nat-src.html index a4e6727e..c2304f09 100644 --- a/Juvix.Builtin.V1.Nat-src.html +++ b/Juvix.Builtin.V1.Nat-src.html @@ -1,5 +1,5 @@ -
module Juvix.Builtin.V1.Nat;
+
module Juvix.Builtin.V1.Nat;
 
 import Juvix.Builtin.V1.Trait.Natural open public;
 import Juvix.Builtin.V1.Trait.FromNatural open public;
@@ -20,4 +20,4 @@
     + := (Nat.+);
     * := (Nat.*);
   };
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
\ 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 d13eca86..1001586b 100644 --- a/Juvix.Builtin.V1.Nat.Base-src.html +++ b/Juvix.Builtin.V1.Nat.Base-src.html @@ -1,5 +1,5 @@ -
module Juvix.Builtin.V1.Nat.Base;
+
module Juvix.Builtin.V1.Nat.Base;
 
 import Juvix.Builtin.V1.Fixity open;
 
@@ -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-11-18 3:38 UTC

\ No newline at end of file
+
\ No newline at end of file diff --git a/Juvix.Builtin.V1.Nat.Base.html b/Juvix.Builtin.V1.Nat.Base.html index a12ddceb..c9b3c358 100644 --- a/Juvix.Builtin.V1.Nat.Base.html +++ b/Juvix.Builtin.V1.Nat.Base.html @@ -1,5 +1,5 @@ -Juvix Documentation
stdlib - 0.0.1

Juvix.Builtin.V1.Nat.Base

Definitions

builtin nat +Juvix Documentation

stdlib - 0.0.1

Juvix.Builtin.V1.Nat.Base

Definitions

builtin nat type NatSource#

Inductive natural numbers. I.e. whole non-negative numbers.

Constructors

| zero
| suc Nat

builtin nat-plus + : Nat -> Nat -> NatSource#

Addition for Nats.

builtin nat-mul * : Nat -> Nat -> NatSource#

Multiplication for Nats.

builtin nat-sub @@ -7,4 +7,4 @@ terminating udiv : Nat -> Nat -> NatSource#

Division for Nats. Returns zero if the first element is zero.

builtin nat-div div (n m : Nat) : NatSource#

Division for Nats.

builtin nat-mod -mod (n m : Nat) : NatSource#

Modulo for Nats.

\ No newline at end of file +mod (n m : Nat) : NatSource#

Modulo for Nats.

\ No newline at end of file diff --git a/Juvix.Builtin.V1.Nat.html b/Juvix.Builtin.V1.Nat.html index eb2dcbd7..22ad2d44 100644 --- a/Juvix.Builtin.V1.Nat.html +++ b/Juvix.Builtin.V1.Nat.html @@ -1,4 +1,4 @@ -Juvix Documentation
stdlib - 0.0.1

Juvix.Builtin.V1.Nat

Definitions

import Juvix.Builtin.V1.Trait.Natural open public

import Juvix.Builtin.V1.Trait.FromNatural open public

import Juvix.Builtin.V1.Nat.Base open hiding {+; *; div; mod} public

instance +Juvix Documentation

stdlib - 0.0.1

Juvix.Builtin.V1.Nat

\ No newline at end of file +naturalNatI : Natural NatSource#

\ No newline at end of file diff --git a/Juvix.Builtin.V1.String-src.html b/Juvix.Builtin.V1.String-src.html index 350c9829..e98dfea5 100644 --- a/Juvix.Builtin.V1.String-src.html +++ b/Juvix.Builtin.V1.String-src.html @@ -1,5 +1,5 @@ -
module Juvix.Builtin.V1.String;
+
module Juvix.Builtin.V1.String;
 
 import Juvix.Builtin.V1.Fixity open;
 
@@ -11,4 +11,4 @@
 --- Concatenation of two ;String;s.
 builtin string-concat
 axiom ++str : String -> String -> String;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
\ No newline at end of file diff --git a/Juvix.Builtin.V1.String.html b/Juvix.Builtin.V1.String.html index f87a77ba..353ad2d0 100644 --- a/Juvix.Builtin.V1.String.html +++ b/Juvix.Builtin.V1.String.html @@ -1,4 +1,4 @@ -Juvix Documentation
stdlib - 0.0.1

Juvix.Builtin.V1.String

Definitions

builtin string +Juvix Documentation

stdlib - 0.0.1

Juvix.Builtin.V1.String

Definitions

builtin string axiom String : TypeSource#

Primitive representation of a sequence of characters.

builtin string-concat -axiom ++str : String -> String -> StringSource#

Concatenation of two Strings.

\ No newline at end of file +axiom ++str : String -> String -> StringSource#

Concatenation of two Strings.

\ No newline at end of file diff --git a/Juvix.Builtin.V1.Trait.FromNatural-src.html b/Juvix.Builtin.V1.Trait.FromNatural-src.html index 490b507e..1c57bf4c 100644 --- a/Juvix.Builtin.V1.Trait.FromNatural-src.html +++ b/Juvix.Builtin.V1.Trait.FromNatural-src.html @@ -1,5 +1,5 @@ -
module Juvix.Builtin.V1.Trait.FromNatural;
+
module Juvix.Builtin.V1.Trait.FromNatural;
 
 import Juvix.Builtin.V1.Nat.Base open using {Nat};
 
@@ -7,4 +7,4 @@
 type FromNatural A := mkFromNatural@{builtin from-nat fromNat : Nat -> A};
 
 open FromNatural public;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
\ No newline at end of file diff --git a/Juvix.Builtin.V1.Trait.FromNatural.html b/Juvix.Builtin.V1.Trait.FromNatural.html index d253f3eb..34432225 100644 --- a/Juvix.Builtin.V1.Trait.FromNatural.html +++ b/Juvix.Builtin.V1.Trait.FromNatural.html @@ -1,4 +1,4 @@ -Juvix Documentation
stdlib - 0.0.1

Juvix.Builtin.V1.Trait.FromNatural

Definitions

trait +Juvix Documentation

stdlib - 0.0.1

Juvix.Builtin.V1.Trait.FromNatural

Definitions

trait type FromNatural ASource#

Constructors

| mkFromNatural@{builtin from-nat - fromNat : Nat -> A}

open FromNatural public

\ No newline at end of file + fromNat : Nat -> A}

open FromNatural public

\ 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 e5a36171..0d48b678 100644 --- a/Juvix.Builtin.V1.Trait.Natural-src.html +++ b/Juvix.Builtin.V1.Trait.Natural-src.html @@ -1,5 +1,5 @@ -
module Juvix.Builtin.V1.Trait.Natural;
+
module Juvix.Builtin.V1.Trait.Natural;
 
 import Juvix.Builtin.V1.Nat.Base open using {Nat};
 import Juvix.Builtin.V1.Fixity open;
@@ -18,4 +18,4 @@
   };
 
 open Natural public;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
\ No newline at end of file diff --git a/Juvix.Builtin.V1.Trait.Natural.html b/Juvix.Builtin.V1.Trait.Natural.html index 96754253..5edbc8a3 100644 --- a/Juvix.Builtin.V1.Trait.Natural.html +++ b/Juvix.Builtin.V1.Trait.Natural.html @@ -1,5 +1,5 @@ -Juvix Documentation
stdlib - 0.0.1

Juvix.Builtin.V1.Trait.Natural

Definitions

trait +Juvix Documentation

stdlib - 0.0.1

Juvix.Builtin.V1.Trait.Natural

Definitions

trait type Natural ASource#

Constructors

| mkNatural@{ {{FromNaturalI}} : FromNatural A; syntax operator + additive; @@ -8,4 +8,4 @@ syntax operator * multiplicative; {-# isabelle-operator: {name: "*", prec: 70, assoc: left} #-} * : A -> A -> A; - }

open Natural public

\ No newline at end of file + }

open Natural public

\ No newline at end of file diff --git a/Stdlib.Cairo.Ec-src.html b/Stdlib.Cairo.Ec-src.html index f8d92391..805fd6dc 100644 --- a/Stdlib.Cairo.Ec-src.html +++ b/Stdlib.Cairo.Ec-src.html @@ -1,5 +1,5 @@ -
--- Functions for various actions on the STARK curve:
+
--- Functions for various actions on the STARK curve:
 --- y^2 = x^3 + alpha * x + beta
 --- where alpha = 1 and beta = 0x6f21413efbe40de150e596d72f7a8c5609ad26c15c915c1f4cdfcb99cee9e89.
 --- The point at infinity is represented as (0, 0).
@@ -131,4 +131,4 @@
   syntax operator * multiplicative;
   * : Field -> Point -> Point := mul;
 end;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
\ No newline at end of file diff --git a/Stdlib.Cairo.Ec.html b/Stdlib.Cairo.Ec.html index 8bcb0875..ceb84808 100644 --- a/Stdlib.Cairo.Ec.html +++ b/Stdlib.Cairo.Ec.html @@ -1,8 +1,8 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Cairo.Ec

Description

Functions for various actions on the STARK curve: y^2 = x^3 + alpha * x + beta where alpha = 1 and beta = 0x6f21413efbe40de150e596d72f7a8c5609ad26c15c915c1f4cdfcb99cee9e89. The point at infinity is represented as (0, 0). Implementation largely follows: https://github.com/starkware-libs/cairo-lang/blob/master/src/starkware/cairo/common/ec.cairo

Definitions

module StarkCurveSource#

ALPHA : FieldSource#

BETA : FieldSource#

ORDER : FieldSource#

GEN_X : FieldSource#

GEN_Y : FieldSource#

builtin ec_point +Juvix Documentation

stdlib - 0.0.1

Stdlib.Cairo.Ec

Description

Functions for various actions on the STARK curve: y^2 = x^3 + alpha * x + beta where alpha = 1 and beta = 0x6f21413efbe40de150e596d72f7a8c5609ad26c15c915c1f4cdfcb99cee9e89. The point at infinity is represented as (0, 0). Implementation largely follows: https://github.com/starkware-libs/cairo-lang/blob/master/src/starkware/cairo/common/ec.cairo

Definitions

module StarkCurveSource#

ALPHA : FieldSource#

BETA : FieldSource#

ORDER : FieldSource#

GEN_X : FieldSource#

GEN_Y : FieldSource#

builtin ec_point type PointSource#

Constructors

| mkPoint@{ x : Field; y : Field; }

module InternalSource#

builtin ec_op axiom ecOp : Point -> Field -> Point -> PointSource#

builtin random_ec_point -axiom randomEcPoint : PointSource#

isOnCurve (point : Point) : BoolSource#

Checks if an EC point is on the STARK curve.

double (point : Point) : PointSource#

Doubles a valid `point` (computes point + point) on the elliptic curve.

add (point1 point2 : Point) : PointSource#

Adds two valid points on the EC.

sub (point1 point2 : Point) : PointSource#

Subtracts point2 from point1 on the EC.

addMul (point1 : Point) (alpha : Field) (point2 : Point) : PointSource#

Computes point1 + alpha * point2 on the elliptic curve. Because the EC operation builtin cannot handle inputs where additions of points with the same x coordinate arise during the computation, this function adds and subtracts a nondeterministic point s to the computation, so that regardless of input, the probability that such additions arise will become negligibly small. The precise computation is therefore: ((point1 + s) + alpha * point2) - s so that the inputs to the builtin itself are (point1 + s), alpha, and point2. Arguments: point1 - an EC point. alpha - the multiplication coefficient of point2 (a field element). point2 - an EC point. Returns: point1 + alpha * point2. Assumptions: point1 and point2 are valid points on the curve.

mul (alpha : Field) (point : Point) : PointSource#

Computes alpha * point on the elliptic curve.

module OperatorsSource#

+ : Point -> Point -> PointSource#

- : Point -> Point -> PointSource#

* : Field -> Point -> PointSource#

\ No newline at end of file +axiom randomEcPoint : PointSource#

isOnCurve (point : Point) : BoolSource#

Checks if an EC point is on the STARK curve.

double (point : Point) : PointSource#

Doubles a valid `point` (computes point + point) on the elliptic curve.

add (point1 point2 : Point) : PointSource#

Adds two valid points on the EC.

sub (point1 point2 : Point) : PointSource#

Subtracts point2 from point1 on the EC.

addMul (point1 : Point) (alpha : Field) (point2 : Point) : PointSource#

Computes point1 + alpha * point2 on the elliptic curve. Because the EC operation builtin cannot handle inputs where additions of points with the same x coordinate arise during the computation, this function adds and subtracts a nondeterministic point s to the computation, so that regardless of input, the probability that such additions arise will become negligibly small. The precise computation is therefore: ((point1 + s) + alpha * point2) - s so that the inputs to the builtin itself are (point1 + s), alpha, and point2. Arguments: point1 - an EC point. alpha - the multiplication coefficient of point2 (a field element). point2 - an EC point. Returns: point1 + alpha * point2. Assumptions: point1 and point2 are valid points on the curve.

mul (alpha : Field) (point : Point) : PointSource#

Computes alpha * point on the elliptic curve.

module OperatorsSource#

+ : Point -> Point -> PointSource#

- : Point -> Point -> PointSource#

* : Field -> Point -> PointSource#

\ No newline at end of file diff --git a/Stdlib.Cairo.Pedersen-src.html b/Stdlib.Cairo.Pedersen-src.html index d759f8a1..d5baa7a7 100644 --- a/Stdlib.Cairo.Pedersen-src.html +++ b/Stdlib.Cairo.Pedersen-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Cairo.Pedersen;
+
module Stdlib.Cairo.Pedersen;
 
 import Stdlib.Data.Field open using {Field};
 import Stdlib.Cairo.Ec as Ec;
@@ -26,4 +26,4 @@
     open ConstantPoints;
     open Ec.Operators;
   in P0 + x * P1 + y * P2;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
\ No newline at end of file diff --git a/Stdlib.Cairo.Pedersen.html b/Stdlib.Cairo.Pedersen.html index ee8b5f33..eccd9727 100644 --- a/Stdlib.Cairo.Pedersen.html +++ b/Stdlib.Cairo.Pedersen.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Cairo.Pedersen

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

Stdlib.Cairo.Pedersen

\ No newline at end of file diff --git a/Stdlib.Cairo.Poseidon-src.html b/Stdlib.Cairo.Poseidon-src.html index 086be309..7e4efdf1 100644 --- a/Stdlib.Cairo.Poseidon-src.html +++ b/Stdlib.Cairo.Poseidon-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Cairo.Poseidon;
+
module Stdlib.Cairo.Poseidon;
 
 import Stdlib.Data.Field open;
 import Stdlib.Data.List open;
@@ -49,4 +49,4 @@
             })
           xs;
   in PoseidonState.s0 (go (mkPoseidonState 0 0 0) list);
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
\ No newline at end of file diff --git a/Stdlib.Cairo.Poseidon.html b/Stdlib.Cairo.Poseidon.html index 9f399b11..6e724d29 100644 --- a/Stdlib.Cairo.Poseidon.html +++ b/Stdlib.Cairo.Poseidon.html @@ -1,8 +1,8 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Cairo.Poseidon

Definitions

builtin poseidon_state +Juvix Documentation

stdlib - 0.0.1

Stdlib.Cairo.Poseidon

Definitions

builtin poseidon_state type PoseidonStateSource#

Constructors

| mkPoseidonState@{ s0 : Field; s1 : Field; s2 : Field; }

builtin poseidon -axiom poseidonHash : PoseidonState -> PoseidonStateSource#

poseidonHash1 (x : Field) : FieldSource#

Hashes one element and retrieves a single field element output.

poseidonHash2 (x y : Field) : FieldSource#

Hashes two elements and retrieves a single field element output.

poseidonHashList (list : List Field) : FieldSource#

Hashes n elements and retrieves a single field element output.

\ No newline at end of file +axiom poseidonHash : PoseidonState -> PoseidonStateSource#

poseidonHash1 (x : Field) : FieldSource#

Hashes one element and retrieves a single field element output.

poseidonHash2 (x y : Field) : FieldSource#

Hashes two elements and retrieves a single field element output.

poseidonHashList (list : List Field) : FieldSource#

Hashes n elements and retrieves a single field element output.

\ No newline at end of file diff --git a/Stdlib.Data.BinaryTree-src.html b/Stdlib.Data.BinaryTree-src.html index 729991db..d864c626 100644 --- a/Stdlib.Data.BinaryTree-src.html +++ b/Stdlib.Data.BinaryTree-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.BinaryTree;
+
module Stdlib.Data.BinaryTree;
 
 import Stdlib.Data.Nat open;
 import Stdlib.Data.List open;
@@ -24,4 +24,4 @@
 
 toList {A} (tree : BinaryTree A) : List A :=
   fold \{e ls rs := e :: ls ++ rs} nil tree;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
\ No newline at end of file diff --git a/Stdlib.Data.BinaryTree.html b/Stdlib.Data.BinaryTree.html index 550a0fa7..ae201e95 100644 --- a/Stdlib.Data.BinaryTree.html +++ b/Stdlib.Data.BinaryTree.html @@ -1,6 +1,6 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.BinaryTree

Definitions

type BinaryTree (A : Type)Source#

Constructors

| leaf
| node@{ +Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.BinaryTree

Definitions

type BinaryTree (A : Type)Source#

Constructors

| leaf
| node@{ left : BinaryTree A; element : A; right : BinaryTree A; - }

fold {A B} (f : A -> B -> B -> B) (acc : B) (tree : BinaryTree A) : BSource#

fold a tree in depth-first order

length {A} (tree : BinaryTree A) : NatSource#

toList {A} (tree : BinaryTree A) : List ASource#

\ No newline at end of file + }

fold {A B} (f : A -> B -> B -> B) (acc : B) (tree : BinaryTree A) : BSource#

fold a tree in depth-first order

length {A} (tree : BinaryTree A) : NatSource#

toList {A} (tree : BinaryTree A) : List ASource#

\ No newline at end of file diff --git a/Stdlib.Data.Bool-src.html b/Stdlib.Data.Bool-src.html index 4255c555..c967a61e 100644 --- a/Stdlib.Data.Bool-src.html +++ b/Stdlib.Data.Bool-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.Bool;
+
module Stdlib.Data.Bool;
 
 import Stdlib.Data.Bool.Base open public;
 import Stdlib.Data.Pair.Base open;
@@ -39,4 +39,4 @@
         | x := "true"
         | else := "false";
   };
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
\ No newline at end of file diff --git a/Stdlib.Data.Bool.Base-src.html b/Stdlib.Data.Bool.Base-src.html index 778c0c6f..6df04d89 100644 --- a/Stdlib.Data.Bool.Base-src.html +++ b/Stdlib.Data.Bool.Base-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.Bool.Base;
+
module Stdlib.Data.Bool.Base;
 
 import Juvix.Builtin.V1.Bool open public;
 import Stdlib.Data.Fixity open;
@@ -40,4 +40,4 @@
 
 builtin assert
 assert (x : Bool) : Bool := x;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
\ No newline at end of file diff --git a/Stdlib.Data.Bool.Base.html b/Stdlib.Data.Bool.Base.html index 4d8d4783..337c1492 100644 --- a/Stdlib.Data.Bool.Base.html +++ b/Stdlib.Data.Bool.Base.html @@ -1,6 +1,6 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Bool.Base

Definitions

import Juvix.Builtin.V1.Bool open public

not : Bool -> BoolSource#

Logical negation.

builtin bool-or +Juvix Documentation

stdlib - 0.0.1

Stdlib.Data.Bool.Base

Definitions

import Juvix.Builtin.V1.Bool open public

not : Bool -> BoolSource#

Logical negation.

builtin bool-or || : Bool -> Bool -> BoolSource#

Logical disjunction. Evaluated lazily. Cannot be partially applied

builtin bool-and && : Bool -> Bool -> BoolSource#

Logical conjunction. Evaluated lazily. Cannot be partially applied.

builtin bool-if ite : {A : Type} -> Bool -> A -> A -> ASource#

Returns the first argument if true, otherwise it returns the second argument. Evaluated lazily. Cannot be partially applied.

or (a b : Bool) : BoolSource#

Logical disjunction.

and (a b : Bool) : BoolSource#

Logical conjunction.

builtin assert -assert (x : Bool) : BoolSource#

\ No newline at end of file +assert (x : Bool) : BoolSource#

\ No newline at end of file diff --git a/Stdlib.Data.Bool.html b/Stdlib.Data.Bool.html index a45bf7e8..40c556f6 100644 --- a/Stdlib.Data.Bool.html +++ b/Stdlib.Data.Bool.html @@ -1,5 +1,5 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Bool

Definitions

import Stdlib.Data.Bool.Base open public

instance +Juvix Documentation

stdlib - 0.0.1

Stdlib.Data.Bool

\ No newline at end of file +showBoolI : Show BoolSource#

\ No newline at end of file diff --git a/Stdlib.Data.Byte-src.html b/Stdlib.Data.Byte-src.html index 9d95d4b3..20eb3d82 100644 --- a/Stdlib.Data.Byte-src.html +++ b/Stdlib.Data.Byte-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.Byte;
+
module Stdlib.Data.Byte;
 
 import Stdlib.Data.Byte.Base open using {Byte} public;
 import Stdlib.Data.Byte.Base as Byte public;
@@ -27,4 +27,4 @@
   mkFromNatural@{
     fromNat := Byte.fromNat;
   };
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
\ No newline at end of file diff --git a/Stdlib.Data.Byte.Base-src.html b/Stdlib.Data.Byte.Base-src.html index 5029b69e..d3cc31a1 100644 --- a/Stdlib.Data.Byte.Base-src.html +++ b/Stdlib.Data.Byte.Base-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.Byte.Base;
+
module Stdlib.Data.Byte.Base;
 
 import Stdlib.Data.Bool.Base open;
 import Stdlib.Data.Fixity open;
@@ -21,4 +21,4 @@
 
 builtin byte-eq
 axiom == : Byte -> Byte -> Bool;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
\ No newline at end of file diff --git a/Stdlib.Data.Byte.Base.html b/Stdlib.Data.Byte.Base.html index 2c50f49c..97c781d2 100644 --- a/Stdlib.Data.Byte.Base.html +++ b/Stdlib.Data.Byte.Base.html @@ -1,6 +1,6 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Byte.Base

Definitions

builtin byte +Juvix Documentation

stdlib - 0.0.1

Stdlib.Data.Byte.Base

Definitions

builtin byte axiom Byte : TypeSource#

An 8-bit unsigned integer.

builtin byte-from-nat axiom fromNat : Nat -> ByteSource#

Converts a Nat to a Byte. It takes the modulus of the input natural number with 256.

builtin byte-to-nat axiom toNat : Byte -> NatSource#

Converts a Byte to the corresponding Nat.

builtin byte-eq -axiom == : Byte -> Byte -> BoolSource#

\ No newline at end of file +axiom == : Byte -> Byte -> BoolSource#

\ No newline at end of file diff --git a/Stdlib.Data.Byte.html b/Stdlib.Data.Byte.html index 2538e58a..f4bad435 100644 --- a/Stdlib.Data.Byte.html +++ b/Stdlib.Data.Byte.html @@ -1,5 +1,5 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Byte

Definitions

import Stdlib.Data.Byte.Base open using {Byte} public

import Stdlib.Data.Byte.Base as Byte public

import Stdlib.Trait.Eq open public

import Stdlib.Trait.Show open public

instance +Juvix Documentation

stdlib - 0.0.1

Stdlib.Data.Byte

Definitions

import Stdlib.Data.Byte.Base open using {Byte} public

import Stdlib.Data.Byte.Base as Byte public

import Stdlib.Trait.Eq open public

import Stdlib.Trait.Show open public

instance eqByteI : Eq ByteSource#

instance showByteI : Show ByteSource#

instance -fromNaturalByteI : FromNatural ByteSource#

\ No newline at end of file +fromNaturalByteI : FromNatural ByteSource#

\ No newline at end of file diff --git a/Stdlib.Data.Field-src.html b/Stdlib.Data.Field-src.html index d3586925..0f362412 100644 --- a/Stdlib.Data.Field-src.html +++ b/Stdlib.Data.Field-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.Field;
+
module Stdlib.Data.Field;
 
 import Stdlib.Data.Field.Base open using {Field} public;
 import Stdlib.Data.Field.Base as Field;
@@ -54,4 +54,4 @@
     integralI := integralFieldI;
     / := (Field./);
   };
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
\ No newline at end of file diff --git a/Stdlib.Data.Field.Base-src.html b/Stdlib.Data.Field.Base-src.html index c7608a9f..4d6758fe 100644 --- a/Stdlib.Data.Field.Base-src.html +++ b/Stdlib.Data.Field.Base-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.Field.Base;
+
module Stdlib.Data.Field.Base;
 
 import Stdlib.Data.Fixity open;
 import Stdlib.Data.Nat.Base open;
@@ -43,4 +43,4 @@
 fromNat (n : Nat) : Field := fromInt (ofNat n);
 
 toInt (f : Field) : Int := ofNat (toNat f);
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
\ No newline at end of file diff --git a/Stdlib.Data.Field.Base.html b/Stdlib.Data.Field.Base.html index 36de6e92..c513e3cb 100644 --- a/Stdlib.Data.Field.Base.html +++ b/Stdlib.Data.Field.Base.html @@ -1,5 +1,5 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Field.Base

Definitions

builtin field +Juvix Documentation

stdlib - 0.0.1

Stdlib.Data.Field.Base

Definitions

builtin field axiom Field : TypeSource#

builtin field-add axiom + : Field -> Field -> FieldSource#

builtin field-sub axiom - : Field -> Field -> FieldSource#

builtin field-mul @@ -7,4 +7,4 @@ axiom / : Field -> Field -> FieldSource#

builtin field-eq axiom == : Field -> Field -> BoolSource#

builtin field-from-int axiom fromInt : Int -> FieldSource#

builtin field-to-nat -axiom toNat : Field -> NatSource#

fromNat (n : Nat) : FieldSource#

toInt (f : Field) : IntSource#

\ No newline at end of file +axiom toNat : Field -> NatSource#

fromNat (n : Nat) : FieldSource#

toInt (f : Field) : IntSource#

\ No newline at end of file diff --git a/Stdlib.Data.Field.html b/Stdlib.Data.Field.html index 81c5b4a8..075e3ca0 100644 --- a/Stdlib.Data.Field.html +++ b/Stdlib.Data.Field.html @@ -1,8 +1,8 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Field

Definitions

import Stdlib.Data.Field.Base open using {Field} public

import Stdlib.Trait.Eq open public

import Stdlib.Trait.Show open public

import Stdlib.Trait.Natural open public

import Stdlib.Trait.Integral open public

import Stdlib.Trait.Numeric open public

instance +Juvix Documentation

stdlib - 0.0.1

Stdlib.Data.Field

\ No newline at end of file +numericFieldI : Numeric FieldSource#

\ No newline at end of file diff --git a/Stdlib.Data.Fixity-src.html b/Stdlib.Data.Fixity-src.html index 07c164ee..97ba33cd 100644 --- a/Stdlib.Data.Fixity-src.html +++ b/Stdlib.Data.Fixity-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.Fixity;
+
module Stdlib.Data.Fixity;
 
 import Juvix.Builtin.V1.Fixity open public;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
\ No newline at end of file diff --git a/Stdlib.Data.Fixity.html b/Stdlib.Data.Fixity.html index c5fa42a1..3a6136ee 100644 --- a/Stdlib.Data.Fixity.html +++ b/Stdlib.Data.Fixity.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Fixity

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

Stdlib.Data.Fixity

\ No newline at end of file diff --git a/Stdlib.Data.Int-src.html b/Stdlib.Data.Int-src.html index 427f5dcf..1e8246cd 100644 --- a/Stdlib.Data.Int-src.html +++ b/Stdlib.Data.Int-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.Int;
+
module Stdlib.Data.Int;
 
 import Stdlib.Data.Int.Base open hiding {+; -; *; div; mod} public;
 -- should be re-exported qualified
@@ -65,4 +65,4 @@
     div := Int.div;
     mod := Int.mod;
   };
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
\ No newline at end of file diff --git a/Stdlib.Data.Int.Base-src.html b/Stdlib.Data.Int.Base-src.html index f5e33afa..495aa4b8 100644 --- a/Stdlib.Data.Int.Base-src.html +++ b/Stdlib.Data.Int.Base-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.Int.Base;
+
module Stdlib.Data.Int.Base;
 
 import Stdlib.Data.Fixity open;
 
@@ -94,4 +94,4 @@
   case int of
     | ofNat n := n
     | negSuc n := suc n;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
\ No newline at end of file diff --git a/Stdlib.Data.Int.Base.html b/Stdlib.Data.Int.Base.html index 5ac519c9..06b9aa94 100644 --- a/Stdlib.Data.Int.Base.html +++ b/Stdlib.Data.Int.Base.html @@ -1,5 +1,5 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Int.Base

Definitions

builtin int +Juvix Documentation

stdlib - 0.0.1

Stdlib.Data.Int.Base

Definitions

builtin int type IntSource#

Inductive integers. I.e. whole numbers that can be positive, zero, or negative.

Constructors

| ofNat Nat

ofNat n represents the integer n

| negSuc Nat

negSuc n represents the integer -(n + 1)

toNat (int : Int) : NatSource#

Converts an Int to a Nat. If the Int is negative, it returns zero.

builtin int-nonneg nonNeg : Int -> BoolSource#

Non-negative predicate for Ints.

builtin int-sub-nat intSubNat (n m : Nat) : IntSource#

Subtraction for Nats.

builtin int-plus @@ -9,4 +9,4 @@ * : Int -> Int -> IntSource#

Multiplication for Ints.

builtin int-sub - (n m : Int) : IntSource#

Subtraction for Ints.

builtin int-div div : Int -> Int -> IntSource#

Division for Ints.

builtin int-mod -mod : Int -> Int -> IntSource#

Modulo for Ints.

abs (int : Int) : NatSource#

Absolute value

\ No newline at end of file +mod : Int -> Int -> IntSource#

Modulo for Ints.

abs (int : Int) : NatSource#

Absolute value

\ No newline at end of file diff --git a/Stdlib.Data.Int.Ord-src.html b/Stdlib.Data.Int.Ord-src.html index 4e71930f..ec8654cc 100644 --- a/Stdlib.Data.Int.Ord-src.html +++ b/Stdlib.Data.Int.Ord-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.Int.Ord;
+
module Stdlib.Data.Int.Ord;
 
 import Stdlib.Data.Fixity open;
 
@@ -59,4 +59,4 @@
 
 --- Returns the biggest ;Int;.
 max (x y : Int) : Int := ite (x > y) x y;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
\ No newline at end of file diff --git a/Stdlib.Data.Int.Ord.html b/Stdlib.Data.Int.Ord.html index b1bc9cc4..05d1b708 100644 --- a/Stdlib.Data.Int.Ord.html +++ b/Stdlib.Data.Int.Ord.html @@ -1,5 +1,5 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Int.Ord

Definitions

builtin int-eq +Juvix Documentation

stdlib - 0.0.1

Stdlib.Data.Int.Ord

Definitions

builtin int-eq == : Int -> Int -> BoolSource#

Tests for equality.

/= (m n : Int) : BoolSource#

Tests for inequality.

builtin int-le <= (m n : Int) : BoolSource#

Returns true iff the first element is less than or equal to the second.

builtin int-lt -< (m n : Int) : BoolSource#

Returns true iff the first element is less than the second.

> (m n : Int) : BoolSource#

Returns true iff the first element is greater than the second.

>= (m n : Int) : BoolSource#

Returns true iff the first element is greater than or equal to the second.

compare (m n : Int) : OrderingSource#

Tests for Ordering.

min (x y : Int) : IntSource#

Returns the smallest Int.

max (x y : Int) : IntSource#

Returns the biggest Int.

\ No newline at end of file +< (m n : Int) : BoolSource#

Returns true iff the first element is less than the second.

> (m n : Int) : BoolSource#

Returns true iff the first element is greater than the second.

>= (m n : Int) : BoolSource#

Returns true iff the first element is greater than or equal to the second.

compare (m n : Int) : OrderingSource#

Tests for Ordering.

min (x y : Int) : IntSource#

Returns the smallest Int.

max (x y : Int) : IntSource#

Returns the biggest Int.

\ No newline at end of file diff --git a/Stdlib.Data.Int.html b/Stdlib.Data.Int.html index ca4f8a86..a6ecb0bd 100644 --- a/Stdlib.Data.Int.html +++ b/Stdlib.Data.Int.html @@ -1,5 +1,5 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Int

Definitions

import Stdlib.Data.Int.Base open hiding {+; -; *; div; mod} public

builtin int-to-string +Juvix Documentation

stdlib - 0.0.1

Stdlib.Data.Int

Definitions

import Stdlib.Data.Int.Base open hiding {+; -; *; div; mod} public

builtin int-to-string axiom intToString : Int -> StringSource#

Converts an Int into String.

instance eqIntI : Eq IntSource#

instance ordIntI : Ord IntSource#

instance @@ -7,4 +7,4 @@ fromNaturalIntI : FromNatural IntSource#

instance naturalIntI : Natural IntSource#

instance integralIntI : Integral IntSource#

instance -divModIntI : DivMod IntSource#

\ No newline at end of file +divModIntI : DivMod IntSource#

\ No newline at end of file diff --git a/Stdlib.Data.List-src.html b/Stdlib.Data.List-src.html index 66b9c218..b17faa3d 100644 --- a/Stdlib.Data.List-src.html +++ b/Stdlib.Data.List-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.List;
+
module Stdlib.Data.List;
 
 import Stdlib.Data.List.Base open public;
 import Stdlib.Data.Bool.Base open;
@@ -14,13 +14,13 @@
 import Stdlib.Trait.Foldable open using {
   Foldable;
   module Polymorphic;
-  fromPolymorphicFoldable;
+  fromPolymorphicFoldable;
 };
 
 --- 𝒪(1). Partial function that returns the first element of a ;List;.
 phead {A} {{Partial}} : List A -> A
   | (x :: _) := x
-  | nil := fail "head: empty list";
+  | nil := fail "head: empty list";
 
 instance
 eqListI {A} {{Eq A}} : Eq (List A) :=
@@ -87,7 +87,7 @@
 
 {-# specialize: true, inline: true #-}
 instance
-foldableListI {A} : Foldable (List A) A := fromPolymorphicFoldable;
+foldableListI {A} : Foldable (List A) A := fromPolymorphicFoldable;
 
 instance
 applicativeListI : Applicative List :=
@@ -95,7 +95,7 @@
     pure {A} (a : A) : List A := [a];
     ap {A B} : (listOfFuns : List (A -> B)) -> (listOfAs : List A) -> List B
       | [] _ := []
-      | (f :: fs) l := map f l ++ ap fs l;
+      | (f :: fs) l := map f l ++ ap fs l;
   };
 
 instance
@@ -103,4 +103,4 @@
   mkMonad@{
     bind := flip concatMap;
   };
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
\ No newline at end of file diff --git a/Stdlib.Data.List.Base-src.html b/Stdlib.Data.List.Base-src.html index aafd7c09..fc6ecf24 100644 --- a/Stdlib.Data.List.Base-src.html +++ b/Stdlib.Data.List.Base-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.List.Base;
+
module Stdlib.Data.List.Base;
 
 import Juvix.Builtin.V1.List open public;
 import Stdlib.Data.Fixity open;
@@ -257,4 +257,4 @@
   | nil := nil
   | (xs :: nil) := listMap λ{x := x :: nil} xs
   | (xs :: xss) := zipWith (::) xs (transpose xss);
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
\ No newline at end of file diff --git a/Stdlib.Data.List.Base.html b/Stdlib.Data.List.Base.html index 969629dc..d8ea38d4 100644 --- a/Stdlib.Data.List.Base.html +++ b/Stdlib.Data.List.Base.html @@ -1,5 +1,5 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.List.Base

Definitions

import Juvix.Builtin.V1.List open public

isElement {A} (eq : A -> A -> Bool) (elem : A) : (list : List A) -> BoolSource#

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

find {A} (predicate : A -> Bool) : (list : List A) -> Maybe ASource#

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

listRfor {A B} (fun : B -> A -> B) (acc : B) : (list : List A) -> BSource#

liftFoldr {A B} (fun : A -> B -> B) (acc : B) (list : List A) : BSource#

Right-associative fold.

listFoldl {A B} (fun : B -> A -> B) (acc : B) : (list : List A) -> BSource#

Left-associative and tail-recursive fold.

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

listMap {A B} (fun : A -> B) : (list : List A) -> List BSource#

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

filter {A} (predicate : A -> Bool) : (list : 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} (list : List A) : NatSource#

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

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

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

replicate {A} : (resultLength : Nat) -> (value : A) -> List ASource#

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

take {A} : (elemsNum : Nat) -> (list : List A) -> List ASource#

Takes the first elemsNum elements of a List.

drop {A} : (elemsNum : Nat) -> (list : List A) -> List ASource#

Drops the first elemsNum elements of a List.

splitAt {A} : (prefixLength : Nat) -> (list : List A) -> Pair (List A) (List A)Source#

𝒪(𝓃). Returns a tuple where first element is the prefix of the given list of length prefixLength 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

isElement {A} (eq : A -> A -> Bool) (elem : A) : (list : List A) -> BoolSource#

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

find {A} (predicate : A -> Bool) : (list : List A) -> Maybe ASource#

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

listRfor {A B} (fun : B -> A -> B) (acc : B) : (list : List A) -> BSource#

liftFoldr {A B} (fun : A -> B -> B) (acc : B) (list : List A) : BSource#

Right-associative fold.

listFoldl {A B} (fun : B -> A -> B) (acc : B) : (list : List A) -> BSource#

Left-associative and tail-recursive fold.

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

listMap {A B} (fun : A -> B) : (list : List A) -> List BSource#

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

filter {A} (predicate : A -> Bool) : (list : 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} (list : List A) : NatSource#

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

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

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

replicate {A} : (resultLength : Nat) -> (value : A) -> List ASource#

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

take {A} : (elemsNum : Nat) -> (list : List A) -> List ASource#

Takes the first elemsNum elements of a List.

drop {A} : (elemsNum : Nat) -> (list : List A) -> List ASource#

Drops the first elemsNum elements of a List.

splitAt {A} : (prefixLength : Nat) -> (list : List A) -> Pair (List A) (List A)Source#

𝒪(𝓃). Returns a tuple where first element is the prefix of the given list of length prefixLength and second element is the remainder of the List.

terminating merge {A} {{Ord A}} (list1 list2 : List A) : List ASource#

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

partition {A} (predicate : A → Bool) : (list : 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} -> (list1 : List A) -> (list2 : List A) -> List ASource#

Concatenates two Lists.

snoc {A} (list : List A) (elem : A) : List ASource#

𝒪(𝓃). Append an element.

flatten {A} (listOfLists : List (List A)) : List ASource#

Concatenates a List of Lists.

prependToAll {A} (separator : A) : (list : List A) -> List ASource#

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

intersperse {A} (separator : A) (list : List A) : List ASource#

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

tail {A} (list : List A) : List ASource#

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

head {A} (defaultValue : A) (list : List A) : ASource#

any {A} (predicate : A -> Bool) : (list : List A) -> BoolSource#

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

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

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

isEmpty {A} (list : List A) : BoolSource#

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

zipWith {A B C} (fun : A -> B -> C) : (list1 : List A) -> (list2 : 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} : (list1 : List A) -> (list2 : List B) -> List (Pair A B)Source#

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

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

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

terminating -quickSort {A} {{Ord A}} (list : List A) : List ASource#

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

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

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

concatMap {A B} (fun : A -> List B) (list : 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} : (listOfLists : List (List A)) -> List (List A)Source#

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

\ No newline at end of file +quickSort {A} {{Ord A}} (list : List A) : List ASource#

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

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

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

concatMap {A B} (fun : A -> List B) (list : 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} : (listOfLists : 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 1e18a53d..00e906ca 100644 --- a/Stdlib.Data.List.html +++ b/Stdlib.Data.List.html @@ -1,5 +1,5 @@ -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 +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#

isMember {A} {{Eq A}} (elem : A) (list : List A) : BoolSource#

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

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

instance @@ -8,4 +8,4 @@ polymorphicFoldableListI : Polymorphic.Foldable ListSource#

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

instance applicativeListI : Applicative ListSource#

instance -monadListI : Monad ListSource#

\ No newline at end of file +monadListI : Monad ListSource#

\ No newline at end of file diff --git a/Stdlib.Data.Map-src.html b/Stdlib.Data.Map-src.html index eed8c1f2..3dd4c8fb 100644 --- a/Stdlib.Data.Map-src.html +++ b/Stdlib.Data.Map-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.Map;
+
module Stdlib.Data.Map;
 
 import Stdlib.Data.Pair open;
 import Stdlib.Data.Maybe open;
@@ -8,8 +8,8 @@
 import Stdlib.Data.Nat open;
 import Stdlib.Data.Bool open;
 
-import Stdlib.Trait.Functor open using {Functor; mkFunctor; map as fmap};
-import Stdlib.Trait.Foldable open hiding {foldr; foldl};
+import Stdlib.Trait.Functor open using {Functor; mkFunctor; map as fmap};
+import Stdlib.Trait.Foldable open hiding {foldr; foldl};
 import Stdlib.Trait.Ord open;
 
 import Stdlib.Function open;
@@ -78,7 +78,7 @@
 {-# specialize: [1] #-}
 lookup
   {Key Value} {{Ord Key}} (key : Key) (map : Map Key Value) : Maybe Value :=
-  case map of mkMap s := fmap value (Set.lookupWith Binding.key key s);
+  case map of mkMap s := fmap value (Set.lookupWith Binding.key key s);
 
 --- 𝒪(log 𝓃). Queries whether a given `key` is in `map`.
 {-# specialize: [1] #-}
@@ -92,7 +92,7 @@
   (fun : Key -> Value -> Value -> Value)
   (list : List (Pair Key Value))
   : Map Key Value :=
-  for (acc := empty) (k, v in list) {
+  for (acc := empty) (k, v in list) {
     insertWith (fun k) k v acc
   };
 
@@ -112,7 +112,7 @@
 toList {Key Value} (map : Map Key Value) : List (Pair Key Value) :=
   case map of
     mkMap s :=
-      fmap (x in Set.toList s) {
+      fmap (x in Set.toList s) {
         toPair x
       };
 
@@ -123,13 +123,13 @@
   (fun : Key -> Value)
   (set : Set Key)
   : Map Key Value :=
-  for (acc := empty) (k in set) {
+  for (acc := empty) (k in set) {
     insert k (fun k) acc
   };
 
 {-# specialize: [1] #-}
 fromSet {Key Value} {{Ord Key}} (set : Set (Pair Key Value)) : Map Key Value :=
-  for (acc := empty) (k, v in set) {
+  for (acc := empty) (k, v in set) {
     insert k v acc
   };
 
@@ -165,14 +165,14 @@
 keys {Key Value} (map : Map Key Value) : List Key :=
   case map of
     mkMap s :=
-      fmap (x in Set.toList s) {
+      fmap (x in Set.toList s) {
         key x
       };
 
 values {Key Value} (map : Map Key Value) : List Value :=
   case map of
     mkMap s :=
-      fmap (x in Set.toList s) {
+      fmap (x in Set.toList s) {
         value x
       };
 
@@ -221,7 +221,7 @@
   : Acc :=
   case map of
     mkMap s :=
-      rfor (acc := acc) (x in s) {
+      rfor (acc := acc) (x in s) {
         fun (key x) (value x) acc
       };
 
@@ -234,7 +234,7 @@
   : Acc :=
   case map of
     mkMap s :=
-      for (acc := acc) (x in s) {
+      for (acc := acc) (x in s) {
         fun acc (key x) (value x)
       };
 
@@ -270,7 +270,7 @@
   {{Foldable Container (Map Key Value)}}
   (maps : Container)
   : Map Key Value :=
-  for (acc := empty) (map in maps) {
+  for (acc := empty) (map in maps) {
     union acc map
   };
 
@@ -373,4 +373,4 @@
 
 instance
 ordMapI {A B} {{Ord A}} {{Ord B}} : Ord (Map A B) := mkOrd (Ord.cmp on toList);
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
\ No newline at end of file diff --git a/Stdlib.Data.Map.html b/Stdlib.Data.Map.html index 90308ae9..1257542d 100644 --- a/Stdlib.Data.Map.html +++ b/Stdlib.Data.Map.html @@ -1,5 +1,5 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Map

Definitions

type Binding Key ValueSource#

Constructors

| mkBinding@{ +Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Map

\ No newline at end of file +ordMapI {A B} {{Ord A}} {{Ord B}} : Ord (Map A B)Source#

\ No newline at end of file diff --git a/Stdlib.Data.Maybe-src.html b/Stdlib.Data.Maybe-src.html index 64f51758..54bf9744 100644 --- a/Stdlib.Data.Maybe-src.html +++ b/Stdlib.Data.Maybe-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.Maybe;
+
module Stdlib.Data.Maybe;
 
 import Stdlib.Data.Maybe.Base open public;
 
@@ -78,4 +78,4 @@
         | nothing := nothing
         | just a := fun a;
   };
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Data.Maybe.Base-src.html b/Stdlib.Data.Maybe.Base-src.html index 44303ba0..22c07575 100644 --- a/Stdlib.Data.Maybe.Base-src.html +++ b/Stdlib.Data.Maybe.Base-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.Maybe.Base;
+
module Stdlib.Data.Maybe.Base;
 
 import Juvix.Builtin.V1.Maybe open public;
 import Juvix.Builtin.V1.Bool open;
@@ -23,4 +23,4 @@
   case maybeValue of
     | nothing := false
     | just _ := true;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Data.Maybe.Base.html b/Stdlib.Data.Maybe.Base.html index 7dfaeff5..0671c716 100644 --- a/Stdlib.Data.Maybe.Base.html +++ b/Stdlib.Data.Maybe.Base.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Maybe.Base

Definitions

import Juvix.Builtin.V1.Maybe open public

fromMaybe {A} (defaultValue : A) (maybeValue : Maybe A) : ASource#

Extracts the value from a Maybe if present, else returns the given value.

maybe {A B} (defaultValue : B) (fun : A -> B) (maybeValue : Maybe A) : BSource#

Applies a function to the value from a Maybe if present, else returns the given value.

isJust {A} (maybeValue : Maybe A) : BoolSource#

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

Stdlib.Data.Maybe.Base

Definitions

import Juvix.Builtin.V1.Maybe open public

fromMaybe {A} (defaultValue : A) (maybeValue : Maybe A) : ASource#

Extracts the value from a Maybe if present, else returns the given value.

maybe {A B} (defaultValue : B) (fun : A -> B) (maybeValue : Maybe A) : BSource#

Applies a function to the value from a Maybe if present, else returns the given value.

isJust {A} (maybeValue : Maybe A) : BoolSource#

\ No newline at end of file diff --git a/Stdlib.Data.Maybe.html b/Stdlib.Data.Maybe.html index f4a42231..4a099f45 100644 --- a/Stdlib.Data.Maybe.html +++ b/Stdlib.Data.Maybe.html @@ -1,9 +1,9 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Maybe

Definitions

import Stdlib.Data.Maybe.Base open public

instance +Juvix Documentation

stdlib - 0.0.1

Stdlib.Data.Maybe

\ No newline at end of file +monadMaybeI : Monad MaybeSource#

\ No newline at end of file diff --git a/Stdlib.Data.Nat-src.html b/Stdlib.Data.Nat-src.html index ae7765f4..8491987a 100644 --- a/Stdlib.Data.Nat-src.html +++ b/Stdlib.Data.Nat-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.Nat;
+
module Stdlib.Data.Nat;
 
 import Juvix.Builtin.V1.Nat open public;
 import Stdlib.Data.Nat.Base open hiding {+; *; div; mod} public;
@@ -43,4 +43,4 @@
     div := Nat.div;
     mod := Nat.mod;
   };
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Data.Nat.Base-src.html b/Stdlib.Data.Nat.Base-src.html index af2b1d3b..7d443a65 100644 --- a/Stdlib.Data.Nat.Base-src.html +++ b/Stdlib.Data.Nat.Base-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.Nat.Base;
+
module Stdlib.Data.Nat.Base;
 
 import Juvix.Builtin.V1.Nat.Base open public;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Data.Nat.Base.html b/Stdlib.Data.Nat.Base.html index c8bf05aa..0ec2f385 100644 --- a/Stdlib.Data.Nat.Base.html +++ b/Stdlib.Data.Nat.Base.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Nat.Base

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

Stdlib.Data.Nat.Base

\ No newline at end of file diff --git a/Stdlib.Data.Nat.Ord-src.html b/Stdlib.Data.Nat.Ord-src.html index 69eeea47..89c8e11b 100644 --- a/Stdlib.Data.Nat.Ord-src.html +++ b/Stdlib.Data.Nat.Ord-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.Nat.Ord;
+
module Stdlib.Data.Nat.Ord;
 
 import Stdlib.Data.Fixity open;
 
@@ -66,4 +66,4 @@
   if 
     | x > y := x
     | else := y;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Data.Nat.Ord.html b/Stdlib.Data.Nat.Ord.html index 05e7ec15..f56a8a9a 100644 --- a/Stdlib.Data.Nat.Ord.html +++ b/Stdlib.Data.Nat.Ord.html @@ -1,5 +1,5 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Nat.Ord

Definitions

builtin nat-eq +Juvix Documentation

stdlib - 0.0.1

Stdlib.Data.Nat.Ord

Definitions

builtin nat-eq == : Nat -> Nat -> BoolSource#

Tests for equality.

/= (x y : Nat) : BoolSource#

Tests for inequality.

builtin nat-le <= : Nat -> Nat -> BoolSource#

Returns true iff the first element is less than or equal to the second.

builtin nat-lt -< (n m : Nat) : BoolSource#

Returns true iff the first element is less than the second.

> (n m : Nat) : BoolSource#

Returns true iff the first element is greater than the second.

>= (n m : Nat) : BoolSource#

Returns true iff the first element is greater than or equal to the second.

compare (n m : Nat) : OrderingSource#

Tests for Ordering.

min (x y : Nat) : NatSource#

Returns the smaller Nat.

max (x y : Nat) : NatSource#

Returns the larger Nat.

\ No newline at end of file +< (n m : Nat) : BoolSource#

Returns true iff the first element is less than the second.

> (n m : Nat) : BoolSource#

Returns true iff the first element is greater than the second.

>= (n m : Nat) : BoolSource#

Returns true iff the first element is greater than or equal to the second.

compare (n m : Nat) : OrderingSource#

Tests for Ordering.

min (x y : Nat) : NatSource#

Returns the smaller Nat.

max (x y : Nat) : NatSource#

Returns the larger Nat.

\ No newline at end of file diff --git a/Stdlib.Data.Nat.html b/Stdlib.Data.Nat.html index 168f2b4a..a5e7d030 100644 --- a/Stdlib.Data.Nat.html +++ b/Stdlib.Data.Nat.html @@ -1,8 +1,8 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Nat

Definitions

import Juvix.Builtin.V1.Nat open public

import Stdlib.Data.Nat.Base open hiding {+; *; div; mod} public

import Stdlib.Trait.Eq open public

import Stdlib.Trait.Ord open public

import Stdlib.Trait.Show open public

import Stdlib.Trait.Natural open public

import Stdlib.Trait.FromNatural open public

import Stdlib.Trait.DivMod open public

builtin nat-to-string +Juvix Documentation

stdlib - 0.0.1

Stdlib.Data.Nat

Definitions

import Juvix.Builtin.V1.Nat open public

import Stdlib.Data.Nat.Base open hiding {+; *; div; mod} public

import Stdlib.Trait.Eq open public

import Stdlib.Trait.Ord open public

import Stdlib.Trait.Show open public

import Stdlib.Trait.Natural open public

import Stdlib.Trait.FromNatural open public

import Stdlib.Trait.DivMod open public

builtin nat-to-string axiom natToString : Nat -> StringSource#

Converts a Nat into a String.

builtin string-to-nat axiom stringToNat : String -> NatSource#

Partial function that converts a String into a Nat.

instance eqNatI : Eq NatSource#

instance ordNatI : Ord NatSource#

instance showNatI : Show NatSource#

instance -divModNatI : DivMod NatSource#

\ No newline at end of file +divModNatI : DivMod NatSource#

\ No newline at end of file diff --git a/Stdlib.Data.Pair-src.html b/Stdlib.Data.Pair-src.html index b7052b51..bd23e6d9 100644 --- a/Stdlib.Data.Pair-src.html +++ b/Stdlib.Data.Pair-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.Pair;
+
module Stdlib.Data.Pair;
 
 import Stdlib.Data.Pair.Base open public;
 import Stdlib.Data.Bool.Base open;
@@ -39,4 +39,4 @@
       show (p : Pair A B) : String :=
         case p of a, b := "(" ++str showA a ++str " , " ++str showB b ++str ")";
     };
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Data.Pair.Base-src.html b/Stdlib.Data.Pair.Base-src.html index f7875afa..e256c3ea 100644 --- a/Stdlib.Data.Pair.Base-src.html +++ b/Stdlib.Data.Pair.Base-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.Pair.Base;
+
module Stdlib.Data.Pair.Base;
 
 import Stdlib.Data.Fixity open;
 
@@ -36,4 +36,4 @@
 --- Applies a function f to both components.
 both {A B} (fun : A -> B) (pair : Pair A A) : Pair B B :=
   case pair of a, b := fun a, fun b;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Data.Pair.Base.html b/Stdlib.Data.Pair.Base.html index e33953ac..2716a0c0 100644 --- a/Stdlib.Data.Pair.Base.html +++ b/Stdlib.Data.Pair.Base.html @@ -1,3 +1,3 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Pair.Base

Definitions

builtin pair -type Pair (A B : Type)Source#

Inductive pair. I.e. a tuple with two components.

Constructors

| , : A → B → Pair A B

uncurry {A B C} (fun : A -> B -> C) (pair : Pair A B) : CSource#

Converts a function f of two arguments to a function with a product argument.

curry {A B C} (fun : Pair A B -> C) (a : A) (b : B) : CSource#

Converts a function f with a product argument to a function of two arguments.

fst {A B} (pair : Pair A B) : ASource#

Projects the first component of a tuple.

snd {A B} (pair : Pair A B) : BSource#

Projects the second component of a tuple.

swap {A B} (pair : Pair A B) : Pair B ASource#

Swaps the components of a tuple.

first {A B A'} (fun : A -> A') (pair : Pair A B) : Pair A' BSource#

Applies a function f to the first component.

second {A B B'} (fun : B -> B') (pair : Pair A B) : Pair A B'Source#

Applies a function f to the second component.

both {A B} (fun : A -> B) (pair : Pair A A) : Pair B BSource#

Applies a function f to both components.

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

Stdlib.Data.Pair.Base

Definitions

builtin pair +type Pair (A B : Type)Source#

Inductive pair. I.e. a tuple with two components.

Constructors

| , : A → B → Pair A B

uncurry {A B C} (fun : A -> B -> C) (pair : Pair A B) : CSource#

Converts a function f of two arguments to a function with a product argument.

curry {A B C} (fun : Pair A B -> C) (a : A) (b : B) : CSource#

Converts a function f with a product argument to a function of two arguments.

fst {A B} (pair : Pair A B) : ASource#

Projects the first component of a tuple.

snd {A B} (pair : Pair A B) : BSource#

Projects the second component of a tuple.

swap {A B} (pair : Pair A B) : Pair B ASource#

Swaps the components of a tuple.

first {A B A'} (fun : A -> A') (pair : Pair A B) : Pair A' BSource#

Applies a function f to the first component.

second {A B B'} (fun : B -> B') (pair : Pair A B) : Pair A B'Source#

Applies a function f to the second component.

both {A B} (fun : A -> B) (pair : Pair A A) : Pair B BSource#

Applies a function f to both components.

\ No newline at end of file diff --git a/Stdlib.Data.Pair.html b/Stdlib.Data.Pair.html index 96aec37d..cacc6169 100644 --- a/Stdlib.Data.Pair.html +++ b/Stdlib.Data.Pair.html @@ -1,5 +1,5 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Pair

Definitions

import Stdlib.Data.Pair.Base open public

instance +Juvix Documentation

stdlib - 0.0.1

Stdlib.Data.Pair

Definitions

import Stdlib.Data.Pair.Base open public

instance eqProductI {A B} : {{Eq A}} -> {{Eq B}} -> Eq (Pair A B)Source#

instance ordProductI {A B} : {{Ord A}} -> {{Ord B}} -> Ord (Pair A B)Source#

instance -showProductI {A B} : {{Show A}} -> {{Show B}} -> Show (Pair A B)Source#

\ No newline at end of file +showProductI {A B} : {{Show A}} -> {{Show B}} -> Show (Pair A B)Source#

\ No newline at end of file diff --git a/Stdlib.Data.Queue-src.html b/Stdlib.Data.Queue-src.html index 3b0b3b2b..9ce0dcb1 100644 --- a/Stdlib.Data.Queue-src.html +++ b/Stdlib.Data.Queue-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.Queue;
+
module Stdlib.Data.Queue;
 
 import Stdlib.Data.Queue.Base open public;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Data.Queue.Base-src.html b/Stdlib.Data.Queue.Base-src.html index 0c101ed5..fb03c9b3 100644 --- a/Stdlib.Data.Queue.Base-src.html +++ b/Stdlib.Data.Queue.Base-src.html @@ -1,5 +1,5 @@ -
--- This module provides an implementation of a First-In, First-Out (FIFO)
+
--- This module provides an implementation of a First-In, First-Out (FIFO)
 --- queue based on Okasaki's "Purely Functional Data Structures." Ch.3.
 ---
 --- This Okasaki Queue version data structure ensures amortized constant-time
@@ -67,7 +67,7 @@
 
 --- 𝒪(n). Adds a list of elements to the end of the ;Queue;.
 pushMany {A} (list : List A) (queue : Queue A) : Queue A :=
-  for (acc := queue) (x in list) {
+  for (acc := queue) (x in list) {
     push x acc
   };
 
@@ -92,4 +92,4 @@
 
 instance
 ordQueueI {A} {{Ord A}} : Ord (Queue A) := mkOrd (Ord.cmp on toList);
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Data.Queue.Base.html b/Stdlib.Data.Queue.Base.html index 92c185cd..1842dbda 100644 --- a/Stdlib.Data.Queue.Base.html +++ b/Stdlib.Data.Queue.Base.html @@ -1,8 +1,8 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Queue.Base

Description

This module provides an implementation of a First-In, First-Out (FIFO) queue based on Okasaki's "Purely Functional Data Structures." Ch.3. This Okasaki Queue version data structure ensures amortized constant-time performance for basic operations such as push, pop, and front. The Okasaki Queue consists of two lists (front and back) to separate the concerns of adding and removing elements for ensuring efficient performance.

Definitions

type Queue (A : Type)Source#

A first-in-first-out data structure

Constructors

| mkQueue@{ +Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Queue.Base

Description

This module provides an implementation of a First-In, First-Out (FIFO) queue based on Okasaki's "Purely Functional Data Structures." Ch.3. This Okasaki Queue version data structure ensures amortized constant-time performance for basic operations such as push, pop, and front. The Okasaki Queue consists of two lists (front and back) to separate the concerns of adding and removing elements for ensuring efficient performance.

Definitions

type Queue (A : Type)Source#

A first-in-first-out data structure

Constructors

| mkQueue@{ front : List A; back : List A; }

empty {A} : Queue ASource#

𝒪(1). The empty Queue.

isEmpty {A} (queue : Queue A) : BoolSource#

𝒪(1). Returns true when the Queue has no elements.

head {A} (queue : Queue A) : Maybe ASource#

𝒪(1). Returns first element of the Queue, if any.

tail {A} (queue : Queue A) : Maybe (Queue A)Source#

𝒪(1). Removes the first element from the Queue. If the Queue is empty

check {A} (queue : Queue A) : Queue ASource#

𝒪(n) worst-case, but 𝒪(1) amortized

pop {A} (queue : Queue A) : Maybe (Pair A (Queue A))Source#

𝒪(n) worst-case, but 𝒪(1) amortized. Returns the first element and the

push {A} (x : A) (queue : Queue A) : Queue ASource#

𝒪(1). Adds an element to the end of the Queue.

pushMany {A} (list : List A) (queue : Queue A) : Queue ASource#

𝒪(n). Adds a list of elements to the end of the Queue.

fromList {A} (list : List A) : Queue ASource#

𝒪(n). Build a Queue from a List.

toList {A} (queue : Queue A) : List ASource#

toList: O(n). Returns a List of the elements in the Queue. The elements are in the same order as they appear in the Queue (i.e. the first element of the Queue is the first element of the List).

size {A} (queue : Queue A) : NatSource#

𝒪(n). Returns the number of elements in the Queue.

instance eqQueueI {A} {{Eq A}} : Eq (Queue A)Source#

instance showQueueI {A} {{Show A}} : Show (Queue A)Source#

instance -ordQueueI {A} {{Ord A}} : Ord (Queue A)Source#

\ No newline at end of file +ordQueueI {A} {{Ord A}} : Ord (Queue A)Source#

\ No newline at end of file diff --git a/Stdlib.Data.Queue.html b/Stdlib.Data.Queue.html index 598288e7..94a8ceea 100644 --- a/Stdlib.Data.Queue.html +++ b/Stdlib.Data.Queue.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Queue

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

Stdlib.Data.Queue

\ No newline at end of file diff --git a/Stdlib.Data.Range-src.html b/Stdlib.Data.Range-src.html index 69b765a0..3415c384 100644 --- a/Stdlib.Data.Range-src.html +++ b/Stdlib.Data.Range-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.Range;
+
module Stdlib.Data.Range;
 
 import Stdlib.Data.Fixity open;
 
@@ -91,4 +91,4 @@
               | else := initialValue;
         in go low;
   };
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Data.Range.html b/Stdlib.Data.Range.html index 708280e1..0a45262b 100644 --- a/Stdlib.Data.Range.html +++ b/Stdlib.Data.Range.html @@ -1,5 +1,5 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Range

Definitions

type Range NSource#

An inclusive range of naturals

Constructors

| mkRange@{ +Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Range

Definitions

type Range NSource#

An inclusive range of naturals

Constructors

| mkRange@{ low : N; high : N; }

type StepRange NSource#

Constructors

| mkStepRange@{ @@ -7,4 +7,4 @@ step : N; }

to {N} {{Natural N}} (low high : N) : Range NSource#

`x to y` is the range [x..y]

step {N} (range : Range N) (step : N) : StepRange NSource#

`x to y step s` is the range [x, x + s, ..., y]

instance foldableRangeI {N} {{Eq N}} {{Natural N}} : Foldable (Range N) NSource#

instance -foldableStepRangeI {N} {{Ord N}} {{Natural N}} : Foldable (StepRange N) NSource#

\ No newline at end of file +foldableStepRangeI {N} {{Ord N}} {{Natural N}} : Foldable (StepRange N) NSource#

\ No newline at end of file diff --git a/Stdlib.Data.Result-src.html b/Stdlib.Data.Result-src.html index c9c7bdfe..1ce605bb 100644 --- a/Stdlib.Data.Result-src.html +++ b/Stdlib.Data.Result-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.Result;
+
module Stdlib.Data.Result;
 
 import Stdlib.Data.Result.Base open public;
 import Stdlib.Data.Bool.Base open;
@@ -84,4 +84,4 @@
         | error e := error e
         | ok a := fun a;
   };
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Data.Result.Base-src.html b/Stdlib.Data.Result.Base-src.html index 9637729d..76160c5a 100644 --- a/Stdlib.Data.Result.Base-src.html +++ b/Stdlib.Data.Result.Base-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.Result.Base;
+
module Stdlib.Data.Result.Base;
 
 import Stdlib.Data.Bool.Base open;
 import Stdlib.Data.Maybe.Base open;
@@ -77,4 +77,4 @@
   case maybeValue of
     | nothing := error defaultError
     | just x := ok x;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Data.Result.Base.html b/Stdlib.Data.Result.Base.html index 4c9c1783..72aa3611 100644 --- a/Stdlib.Data.Result.Base.html +++ b/Stdlib.Data.Result.Base.html @@ -1,5 +1,5 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Result.Base

Definitions

type Result Error ValueSource#

The Result type represents either a success with a value of `ok` or an error with value `error`.

Constructors

| error Error
| ok Value

handleResult +Juvix Documentation

stdlib - 0.0.1

Stdlib.Data.Result.Base

Definitions

type Result Error ValueSource#

The Result type represents either a success with a value of `ok` or an error with value `error`.

Constructors

| error Error
| ok Value

handleResult {Error Value1 Value2} (onError : Error -> Value2) (onOk : Value1 -> Value2) @@ -18,4 +18,4 @@ {Error Value} (defaultError : Error) (maybeValue : Maybe Value) - : Result Error ValueSource#

Convert a Maybe to a Result. A nothing value becomes `error defaultError`.

\ No newline at end of file + : Result Error ValueSource#

Convert a Maybe to a Result. A nothing value becomes `error defaultError`.

\ No newline at end of file diff --git a/Stdlib.Data.Result.html b/Stdlib.Data.Result.html index 3da391f5..1d010c63 100644 --- a/Stdlib.Data.Result.html +++ b/Stdlib.Data.Result.html @@ -1,5 +1,5 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Result

\ No newline at end of file diff --git a/Stdlib.Data.Set-src.html b/Stdlib.Data.Set-src.html index 9dcef61e..74853acc 100644 --- a/Stdlib.Data.Set-src.html +++ b/Stdlib.Data.Set-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.Set;
+
module Stdlib.Data.Set;
 
 import Stdlib.Data.Set.AVL open public;
 import Stdlib.Trait.Eq as Eq open using {Eq};
@@ -10,4 +10,4 @@
 eqSetI {A} {{Eq A}} : Eq (Set A) := eqAVLTreeI;
 
 ordSetI {A} {{Ord A}} : Ord (Set A) := ordAVLTreeI;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Data.Set.AVL-src.html b/Stdlib.Data.Set.AVL-src.html index b48f3f3c..b0bcc225 100644 --- a/Stdlib.Data.Set.AVL-src.html +++ b/Stdlib.Data.Set.AVL-src.html @@ -1,5 +1,5 @@ -
--- AVL trees are a type of self-balancing binary search tree, where the heights
+
--- AVL trees are a type of self-balancing binary search tree, where the heights
 --- of the left and right subtrees of every node differ by at most 1. This
 --- ensures that the height of the tree is logarithmic in the number of nodes,
 --- which guarantees efficient insertion, deletion, and search operations (all
@@ -18,7 +18,7 @@
 import Stdlib.Data.Pair open;
 import Stdlib.Data.List open using {List; nil; ::; filter; ++; catMaybes};
 import Stdlib.Data.String open;
-import Stdlib.Trait.Foldable open hiding {foldr; foldl};
+import Stdlib.Trait.Foldable open hiding {foldr; foldl};
 import Stdlib.Function open;
 
 --- A self-balancing binary search tree.
@@ -270,14 +270,14 @@
   (toDelete : List B)
   (set : AVLTree A)
   : AVLTree A :=
-  for (acc := set) (x in toDelete) {
+  for (acc := set) (x in toDelete) {
     deleteWith fun x acc
   };
 
 --- 𝒪(𝓃 log 𝓃). Create a set from an unsorted ;List;.
 {-# specialize: [1] #-}
 fromList {A} {{Ord A}} (list : List A) : AVLTree A :=
-  for (acc := empty) (x in list) {
+  for (acc := empty) (x in list) {
     insert x acc
   };
 
@@ -319,18 +319,18 @@
 
 {-# specialize: true, inline: true #-}
 instance
-foldableAVLTreeI {A} : Foldable (AVLTree A) A := fromPolymorphicFoldable;
+foldableAVLTreeI {A} : Foldable (AVLTree A) A := fromPolymorphicFoldable;
 
 --- 𝒪(n). Returns the elements of `set` in ascending order.
 toList {A} (set : AVLTree A) : List A :=
-  rfor (acc := nil) (x in set) {
+  rfor (acc := nil) (x in set) {
     x :: acc
   };
 
 --- 𝒪(n log n). Returns a set containing the elements that are members of `set1` and `set2`.
 {-# specialize: [1] #-}
 intersection {A} {{Ord A}} (set1 set2 : AVLTree A) : AVLTree A :=
-  for (acc := empty) (x in set1) {
+  for (acc := empty) (x in set1) {
     if 
       | isMember x set2 := insert x acc
       | else := acc
@@ -339,7 +339,7 @@
 --- 𝒪(n log n). Returns a set containing the elements that are members of `set1` but not of `set2`.
 {-# specialize: [1] #-}
 difference {A} {{Ord A}} (set1 set2 : AVLTree A) : AVLTree A :=
-  for (acc := empty) (x in set1) {
+  for (acc := empty) (x in set1) {
     if 
       | isMember x set2 := acc
       | else := insert x acc
@@ -350,7 +350,7 @@
 --- prefers `set1` when duplicate elements are encountered.
 {-# specialize: [1] #-}
 unionLeft {A} {{Ord A}} (set1 set2 : AVLTree A) : AVLTree A :=
-  for (acc := set2) (x in set1) {
+  for (acc := set2) (x in set1) {
     insert x acc
   };
 
@@ -369,7 +369,7 @@
   {{Foldable Container (AVLTree Elem)}}
   (sets : Container)
   : AVLTree Elem :=
-  for (acc := empty) (set in sets) {
+  for (acc := empty) (set in sets) {
     union acc set
   };
 
@@ -380,7 +380,7 @@
 disjointUnion {A} {{Ord A}} (set1 set2 : AVLTree A) : Result A (AVLTree A) :=
   let
     goUnion (set1 set2 : AVLTree A) : Result A (AVLTree A) :=
-      for (acc := ok set2) (x in set1) {
+      for (acc := ok set2) (x in set1) {
         case acc of
           | error _ := acc
           | ok set :=
@@ -416,7 +416,7 @@
 --- 𝒪(n log n). Returns a set containing all elements of `set` that satisfy `predicate`.
 {-# specialize: [1] #-}
 filter {A} {{Ord A}} (predicate : A -> Bool) (set : AVLTree A) : AVLTree A :=
-  for (acc := empty) (x in set) {
+  for (acc := empty) (x in set) {
     if 
       | predicate x := insert x acc
       | else := acc
@@ -429,7 +429,7 @@
   (predicate : A -> Bool)
   (set : AVLTree A)
   : Pair (AVLTree A) (AVLTree A) :=
-  for (trueSet, falseSet := empty, empty) (x in set) {
+  for (trueSet, falseSet := empty, empty) (x in set) {
     if 
       | predicate x := insert x trueSet, falseSet
       | else := trueSet, insert x falseSet
@@ -446,7 +446,7 @@
 
 syntax iterator map {init := 0; range := 1};
 map {A B} {{Ord B}} (fun : A -> B) (set : AVLTree A) : AVLTree B :=
-  for (acc := empty) (x in set) {
+  for (acc := empty) (x in set) {
     insert (fun x) acc
   };
 
@@ -482,4 +482,4 @@
 
 instance
 ordAVLTreeI {A} {{Ord A}} : Ord (AVLTree A) := mkOrd (Ord.cmp on toList);
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Data.Set.AVL.html b/Stdlib.Data.Set.AVL.html index c949af28..f1739c59 100644 --- a/Stdlib.Data.Set.AVL.html +++ b/Stdlib.Data.Set.AVL.html @@ -1,5 +1,5 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Set.AVL

Description

AVL trees are a type of self-balancing binary search tree, where the heights of the left and right subtrees of every node differ by at most 1. This ensures that the height of the tree is logarithmic in the number of nodes, which guarantees efficient insertion, deletion, and search operations (all are guaranteed to run in 𝒪(log 𝓃) time). This module defines an AVL tree data type and provides functions for constructing, modifying, and querying AVL trees.

Definitions

type AVLTree (A : Type)Source#

A self-balancing binary search tree.

Constructors

| empty

An empty AVL tree.

| node@{ +Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Set.AVL

Description

AVL trees are a type of self-balancing binary search tree, where the heights of the left and right subtrees of every node differ by at most 1. This ensures that the height of the tree is logarithmic in the number of nodes, which guarantees efficient insertion, deletion, and search operations (all are guaranteed to run in 𝒪(log 𝓃) time). This module defines an AVL tree data type and provides functions for constructing, modifying, and querying AVL trees.

Definitions

type AVLTree (A : Type)Source#

A self-balancing binary search tree.

Constructors

| empty

An empty AVL tree.

| node@{ element : A; height : Nat; left : AVLTree A; @@ -39,4 +39,4 @@ (set : AVLTree A) : Pair (AVLTree A) (AVLTree A)Source#

singleton {A} (elem : A) : AVLTree ASource#

𝒪(1). Creates a set with a single element `elem`.

isSubset {A} {{Ord A}} (set1 set2 : AVLTree A) : BoolSource#

𝒪(n log n). Checks if all elements of `set1` are in `set2`.

map {A B} {{Ord B}} (fun : A -> B) (set : AVLTree A) : AVLTree BSource#

prettyDebug {A} {{Show A}} (set : AVLTree A) : StringSource#

Formats the set in a debug friendly format.

toTree {A} : (set : AVLTree A) -> Maybe (Tree A)Source#

𝒪(𝓃).

pretty {A} {{Show A}} (set : AVLTree A) : StringSource#

Returns the textual representation of an AVLTree.

instance eqAVLTreeI {A} {{Eq A}} : Eq (AVLTree A)Source#

instance -ordAVLTreeI {A} {{Ord A}} : Ord (AVLTree A)Source#

\ No newline at end of file +ordAVLTreeI {A} {{Ord A}} : Ord (AVLTree A)Source#

\ No newline at end of file diff --git a/Stdlib.Data.Set.html b/Stdlib.Data.Set.html index 36339fec..7d5d338d 100644 --- a/Stdlib.Data.Set.html +++ b/Stdlib.Data.Set.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Set

Definitions

import Stdlib.Data.Set.AVL open public

syntax alias Set := AVLTreeSource#

eqSetI {A} {{Eq A}} : Eq (Set A)Source#

ordSetI {A} {{Ord A}} : Ord (Set A)Source#

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

Stdlib.Data.Set

Definitions

import Stdlib.Data.Set.AVL open public

syntax alias Set := AVLTreeSource#

eqSetI {A} {{Eq A}} : Eq (Set A)Source#

ordSetI {A} {{Ord A}} : Ord (Set A)Source#

\ No newline at end of file diff --git a/Stdlib.Data.String-src.html b/Stdlib.Data.String-src.html index 1930733f..e3a74ff5 100644 --- a/Stdlib.Data.String-src.html +++ b/Stdlib.Data.String-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.String;
+
module Stdlib.Data.String;
 
 import Stdlib.Data.String.Base open public;
 
@@ -16,4 +16,4 @@
   let
     go (s : String) : String := "\"" ++str s ++str "\"";
   in mkShow go;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Data.String.Base-src.html b/Stdlib.Data.String.Base-src.html index 35cf7f78..982c5668 100644 --- a/Stdlib.Data.String.Base-src.html +++ b/Stdlib.Data.String.Base-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.String.Base;
+
module Stdlib.Data.String.Base;
 
 import Juvix.Builtin.V1.String open public;
 import Stdlib.Data.List.Base open;
@@ -11,4 +11,4 @@
 
 --- Joins a ;List; of ;String;s with "\n".
 unlines (list : List String) : String := concatStr (intersperse "\n" list);
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Data.String.Base.html b/Stdlib.Data.String.Base.html index 68ff6c5d..03d657eb 100644 --- a/Stdlib.Data.String.Base.html +++ b/Stdlib.Data.String.Base.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.String.Base

Definitions

import Juvix.Builtin.V1.String open public

concatStr (string : List String) : StringSource#

Concatenates a List of Strings.

unlines (list : List String) : StringSource#

Joins a List of Strings with "\n".

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

Stdlib.Data.String.Base

Definitions

import Juvix.Builtin.V1.String open public

concatStr (string : List String) : StringSource#

Concatenates a List of Strings.

unlines (list : List String) : StringSource#

Joins a List of Strings with "\n".

\ No newline at end of file diff --git a/Stdlib.Data.String.Ord-src.html b/Stdlib.Data.String.Ord-src.html index a0482772..9fecb236 100644 --- a/Stdlib.Data.String.Ord-src.html +++ b/Stdlib.Data.String.Ord-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.String.Ord;
+
module Stdlib.Data.String.Ord;
 
 import Stdlib.Data.Fixity open;
 
@@ -10,4 +10,4 @@
 --- Equality for ;String;s.
 builtin string-eq
 axiom == : String -> String -> Bool;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Data.String.Ord.html b/Stdlib.Data.String.Ord.html index e83b0b53..77b77195 100644 --- a/Stdlib.Data.String.Ord.html +++ b/Stdlib.Data.String.Ord.html @@ -1,3 +1,3 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.String.Ord

Definitions

builtin string-eq -axiom == : String -> String -> BoolSource#

Equality for Strings.

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

Stdlib.Data.String.Ord

Definitions

builtin string-eq +axiom == : String -> String -> BoolSource#

Equality for Strings.

\ No newline at end of file diff --git a/Stdlib.Data.String.html b/Stdlib.Data.String.html index 29f8823a..329cf9f1 100644 --- a/Stdlib.Data.String.html +++ b/Stdlib.Data.String.html @@ -1,4 +1,4 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.String

Definitions

import Stdlib.Data.String.Base open public

instance +Juvix Documentation

stdlib - 0.0.1

Stdlib.Data.String

\ No newline at end of file +showStringI : Show StringSource#

\ No newline at end of file diff --git a/Stdlib.Data.Tree-src.html b/Stdlib.Data.Tree-src.html index bf984550..d8f9a95c 100644 --- a/Stdlib.Data.Tree-src.html +++ b/Stdlib.Data.Tree-src.html @@ -1,5 +1,5 @@ -
--- N-Ary trees with pretty printing.
+
--- N-Ary trees with pretty printing.
 module Stdlib.Data.Tree;
 
 import Stdlib.Data.List open;
@@ -35,4 +35,4 @@
 
 forestToString {A} {{Show A}} (forest : Forest A) : String :=
   unlines (drawForest forest);
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Data.Tree.html b/Stdlib.Data.Tree.html index bf934822..cc801d97 100644 --- a/Stdlib.Data.Tree.html +++ b/Stdlib.Data.Tree.html @@ -1,7 +1,7 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Tree

Description

N-Ary trees with pretty printing.

Definitions

Forest (A : Type) : TypeSource#

A List of trees.

type Tree (A : Type)Source#

N-Ary tree.

Constructors

| node@{ +Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Tree

Description

N-Ary trees with pretty printing.

Definitions

Forest (A : Type) : TypeSource#

A List of trees.

type Tree (A : Type)Source#

N-Ary tree.

Constructors

| node@{ element : A; children : List (Tree A); }

terminating draw {A} {{Show A}} (tree : Tree A) : List StringSource#

terminating -drawForest {A} {{Show A}} (forest : Forest A) : List StringSource#

treeToString {A} {{Show A}} (tree : Tree A) : StringSource#

forestToString {A} {{Show A}} (forest : Forest A) : StringSource#

\ No newline at end of file +drawForest {A} {{Show A}} (forest : Forest A) : List StringSource#

treeToString {A} {{Show A}} (tree : Tree A) : StringSource#

forestToString {A} {{Show A}} (forest : Forest A) : StringSource#

\ No newline at end of file diff --git a/Stdlib.Data.UnbalancedSet-src.html b/Stdlib.Data.UnbalancedSet-src.html index 8123997a..17b1e038 100644 --- a/Stdlib.Data.UnbalancedSet-src.html +++ b/Stdlib.Data.UnbalancedSet-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Data.UnbalancedSet;
+
module Stdlib.Data.UnbalancedSet;
 
 import Stdlib.Prelude open;
 
@@ -53,4 +53,4 @@
   mkOrd@{
     cmp (s1 s2 : UnbalancedSet A) : Ordering := Ord.cmp (toList s1) (toList s2);
   };
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Data.UnbalancedSet.html b/Stdlib.Data.UnbalancedSet.html index 5cd0debb..1b479b68 100644 --- a/Stdlib.Data.UnbalancedSet.html +++ b/Stdlib.Data.UnbalancedSet.html @@ -1,6 +1,6 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.UnbalancedSet

Definitions

type UnbalancedSet (A : Type)Source#

Constructors

| mkUnbalancedSet@{ +Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.UnbalancedSet

\ No newline at end of file +ordUnbalancedSetI {A} {{Ord A}} : Ord (UnbalancedSet A)Source#

\ No newline at end of file diff --git a/Stdlib.Data.Unit-src.html b/Stdlib.Data.Unit-src.html index 2e2ce5b7..7e89a998 100644 --- a/Stdlib.Data.Unit-src.html +++ b/Stdlib.Data.Unit-src.html @@ -1,5 +1,5 @@ -
--- The unit type.
+
--- The unit type.
 module Stdlib.Data.Unit;
 
 import Stdlib.Data.Unit.Base open public;
@@ -48,4 +48,4 @@
       (_ : Unit)
       : Acc := fun initialValue unit;
   };
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Data.Unit.Base-src.html b/Stdlib.Data.Unit.Base-src.html index 9b39a7cb..ad88b6fc 100644 --- a/Stdlib.Data.Unit.Base-src.html +++ b/Stdlib.Data.Unit.Base-src.html @@ -1,5 +1,5 @@ -
--- The unit type.
+
--- The unit type.
 module Stdlib.Data.Unit.Base;
 
 import Stdlib.Data.Bool.Base open;
@@ -12,4 +12,4 @@
 type Unit :=
   --- The only constructor of ;Unit;.
   unit;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Data.Unit.Base.html b/Stdlib.Data.Unit.Base.html index 4721591d..fbf8f48e 100644 --- a/Stdlib.Data.Unit.Base.html +++ b/Stdlib.Data.Unit.Base.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Unit.Base

Description

The unit type.

Definitions

type UnitSource#

Constructors

| unit

The only constructor of Unit.

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

Stdlib.Data.Unit.Base

Description

The unit type.

Definitions

type UnitSource#

Constructors

| unit

The only constructor of Unit.

\ No newline at end of file diff --git a/Stdlib.Data.Unit.html b/Stdlib.Data.Unit.html index 37c05990..ffa04d56 100644 --- a/Stdlib.Data.Unit.html +++ b/Stdlib.Data.Unit.html @@ -1,6 +1,6 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Unit

Description

The unit type.

Definitions

import Stdlib.Data.Unit.Base open public

instance +Juvix Documentation

stdlib - 0.0.1

Stdlib.Data.Unit

Description

The unit type.

\ No newline at end of file +foldableUnitI : Foldable Unit UnitSource#

\ No newline at end of file diff --git a/Stdlib.Debug-src.html b/Stdlib.Debug-src.html index 5c9a42db..975425b1 100644 --- a/Stdlib.Debug-src.html +++ b/Stdlib.Debug-src.html @@ -1,6 +1,6 @@ -
module Stdlib.Debug;
+
module Stdlib.Debug;
 
 import Stdlib.Debug.Trace open public;
 import Stdlib.Debug.Fail open public;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Debug.Fail-src.html b/Stdlib.Debug.Fail-src.html index 598ebee2..2abe48cf 100644 --- a/Stdlib.Debug.Fail-src.html +++ b/Stdlib.Debug.Fail-src.html @@ -1,9 +1,9 @@ -
module Stdlib.Debug.Fail;
+
module Stdlib.Debug.Fail;
 
 import Stdlib.Data.String.Base open;
 
 --- Exit the program with an error message.
 builtin fail
 axiom failwith : {A : Type} -> (message : String) -> A;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Debug.Fail.html b/Stdlib.Debug.Fail.html index 2fbd07a9..22a6f6c6 100644 --- a/Stdlib.Debug.Fail.html +++ b/Stdlib.Debug.Fail.html @@ -1,3 +1,3 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Debug.Fail

Definitions

builtin fail -axiom failwith : {A : Type} -> (message : String) -> ASource#

Exit the program with an error message.

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

Stdlib.Debug.Fail

Definitions

builtin fail +axiom failwith : {A : Type} -> (message : String) -> ASource#

Exit the program with an error message.

\ No newline at end of file diff --git a/Stdlib.Debug.Trace-src.html b/Stdlib.Debug.Trace-src.html index 32c0003f..4c716d96 100644 --- a/Stdlib.Debug.Trace-src.html +++ b/Stdlib.Debug.Trace-src.html @@ -1,7 +1,7 @@ -
module Stdlib.Debug.Trace;
+
module Stdlib.Debug.Trace;
 
 --- Primitive that prints the given element and returns it.
 builtin trace
 axiom trace : {A : Type} -> A -> A;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Debug.Trace.html b/Stdlib.Debug.Trace.html index 9195f93f..1c0d0209 100644 --- a/Stdlib.Debug.Trace.html +++ b/Stdlib.Debug.Trace.html @@ -1,3 +1,3 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Debug.Trace

Definitions

builtin trace -axiom trace : {A : Type} -> A -> ASource#

Primitive that prints the given element and returns it.

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

Stdlib.Debug.Trace

Definitions

builtin trace +axiom trace : {A : Type} -> A -> ASource#

Primitive that prints the given element and returns it.

\ No newline at end of file diff --git a/Stdlib.Debug.html b/Stdlib.Debug.html index c93c6656..1c433b55 100644 --- a/Stdlib.Debug.html +++ b/Stdlib.Debug.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Debug

Definitions

import Stdlib.Debug.Trace open public

import Stdlib.Debug.Fail open public

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

Stdlib.Debug

Definitions

import Stdlib.Debug.Trace open public

import Stdlib.Debug.Fail open public

\ No newline at end of file diff --git a/Stdlib.Extra.Gcd-src.html b/Stdlib.Extra.Gcd-src.html index 1b2755e4..40176372 100644 --- a/Stdlib.Extra.Gcd-src.html +++ b/Stdlib.Extra.Gcd-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Extra.Gcd;
+
module Stdlib.Extra.Gcd;
 
 import Stdlib.Trait.Natural open;
 import Stdlib.Trait.DivMod open;
@@ -20,4 +20,4 @@
   in if 
     | a > b := gcd' b a
     | else := gcd' a b;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Extra.Gcd.html b/Stdlib.Extra.Gcd.html index 373dc139..723c1dae 100644 --- a/Stdlib.Extra.Gcd.html +++ b/Stdlib.Extra.Gcd.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Extra.Gcd

Definitions

gcd {A} {{Eq A}} {{Ord A}} {{Natural A}} {{DivMod A}} (a b : A) : ASource#

Computes the greatest common divisor of `a` and `b`.

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

Stdlib.Extra.Gcd

Definitions

gcd {A} {{Eq A}} {{Ord A}} {{Natural A}} {{DivMod A}} (a b : A) : ASource#

Computes the greatest common divisor of `a` and `b`.

\ No newline at end of file diff --git a/Stdlib.Function-src.html b/Stdlib.Function-src.html index 3b28daaa..57913597 100644 --- a/Stdlib.Function-src.html +++ b/Stdlib.Function-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Function;
+
module Stdlib.Function;
 
 import Stdlib.Data.Fixity open;
 import Stdlib.Data.Nat.Base open;
@@ -56,4 +56,4 @@
 builtin seq
 >-> : {A B : Type} -> A -> B -> B
   | x y := y;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Function.html b/Stdlib.Function.html index 1a66a2eb..3a000127 100644 --- a/Stdlib.Function.html +++ b/Stdlib.Function.html @@ -1,3 +1,3 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Function

Definitions

<< {A B C} (f : B -> C) (g : A -> B) (x : A) : CSource#

Function composition, passing results from the second function `g` to the first function `f`.

>> {A B C} (f : A -> B) (g : B -> C) (x : A) : CSource#

Function composition, passing results from the first function `f` to the second function `g`.

const {A B} (a : A) (_ : B) : ASource#

Always returns the first argument `a`.

id {A} (a : A) : ASource#

The identity function.

flip {A B C} (f : A -> B -> C) (b : B) (a : A) : CSource#

Swaps the order of the arguments of the given function `f`.

<| {A B} (f : A -> B) (x : A) : BSource#

Application operator with right associativity. Usually used as a syntactical facility.

|> {A B} (x : A) (f : A -> B) : BSource#

Application operator with left associativity. Usually used as a syntactical facility.

iterate {A} : (n : Nat) -> (fun : A -> A) -> (elem : A) -> ASource#

Applies a function n times.

on {A B C} (f : B -> B -> C) (g : A -> B) (a b : A) : CSource#

`(f on g) a b` is equivalent to `f (g a) (g b)`.

builtin seq ->-> : {A B : Type} -> A -> B -> BSource#

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

Stdlib.Function

Definitions

<< {A B C} (f : B -> C) (g : A -> B) (x : A) : CSource#

Function composition, passing results from the second function `g` to the first function `f`.

>> {A B C} (f : A -> B) (g : B -> C) (x : A) : CSource#

Function composition, passing results from the first function `f` to the second function `g`.

const {A B} (a : A) (_ : B) : ASource#

Always returns the first argument `a`.

id {A} (a : A) : ASource#

The identity function.

flip {A B C} (f : A -> B -> C) (b : B) (a : A) : CSource#

Swaps the order of the arguments of the given function `f`.

<| {A B} (f : A -> B) (x : A) : BSource#

Application operator with right associativity. Usually used as a syntactical facility.

|> {A B} (x : A) (f : A -> B) : BSource#

Application operator with left associativity. Usually used as a syntactical facility.

iterate {A} : (n : Nat) -> (fun : A -> A) -> (elem : A) -> ASource#

Applies a function n times.

on {A B C} (f : B -> B -> C) (g : A -> B) (a b : A) : CSource#

`(f on g) a b` is equivalent to `f (g a) (g b)`.

builtin seq +>-> : {A B : Type} -> A -> B -> BSource#

\ No newline at end of file diff --git a/Stdlib.Prelude-src.html b/Stdlib.Prelude-src.html index 2acb06f4..0122e97f 100644 --- a/Stdlib.Prelude-src.html +++ b/Stdlib.Prelude-src.html @@ -1,5 +1,5 @@ -
--- This module reexports most of the standard library.
+
--- This module reexports most of the standard library.
 module Stdlib.Prelude;
 
 import Stdlib.Data.Fixity open public;
@@ -20,4 +20,4 @@
 import Stdlib.System.IO open public;
 
 import Stdlib.Trait open public;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Prelude.html b/Stdlib.Prelude.html index d818b5c3..828d26c7 100644 --- a/Stdlib.Prelude.html +++ b/Stdlib.Prelude.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Prelude

Description

This module reexports most of the standard library.

Definitions

import Stdlib.Data.Fixity open public

import Stdlib.Data.Bool open public

import Stdlib.Data.Byte open public

import Stdlib.Data.Unit open public

import Stdlib.Data.List open public

import Stdlib.Data.Maybe open public

import Stdlib.Data.Nat open public

import Stdlib.Data.Int open public

import Stdlib.Data.Field open public

import Stdlib.Data.Pair open public

import Stdlib.Data.String open public

import Stdlib.Data.Result open public

import Stdlib.Data.Range open public

import Stdlib.Function open public

import Stdlib.System.IO open public

import Stdlib.Trait open public

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

Stdlib.Prelude

Description

This module reexports most of the standard library.

Definitions

import Stdlib.Data.Fixity open public

import Stdlib.Data.Bool open public

import Stdlib.Data.Byte open public

import Stdlib.Data.Unit open public

import Stdlib.Data.List open public

import Stdlib.Data.Maybe open public

import Stdlib.Data.Nat open public

import Stdlib.Data.Int open public

import Stdlib.Data.Field open public

import Stdlib.Data.Pair open public

import Stdlib.Data.String open public

import Stdlib.Data.Result open public

import Stdlib.Data.Range open public

import Stdlib.Function open public

import Stdlib.System.IO open public

import Stdlib.Trait open public

\ No newline at end of file diff --git a/Stdlib.System.IO-src.html b/Stdlib.System.IO-src.html index 89a45779..8069b1d2 100644 --- a/Stdlib.System.IO-src.html +++ b/Stdlib.System.IO-src.html @@ -1,5 +1,5 @@ -
module Stdlib.System.IO;
+
module Stdlib.System.IO;
 
 import Stdlib.System.IO.Base open public;
 import Stdlib.System.IO.Bool open public;
@@ -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-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.System.IO.Base-src.html b/Stdlib.System.IO.Base-src.html index b3c53da0..fedd205e 100644 --- a/Stdlib.System.IO.Base-src.html +++ b/Stdlib.System.IO.Base-src.html @@ -1,5 +1,5 @@ -
module Stdlib.System.IO.Base;
+
module Stdlib.System.IO.Base;
 
 import Stdlib.Data.Fixity open;
 
@@ -9,4 +9,4 @@
 syntax operator >>> seq;
 builtin IO-sequence
 axiom >>> : IO -> IO -> IO;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.System.IO.Base.html b/Stdlib.System.IO.Base.html index 6314d677..9cd463a1 100644 --- a/Stdlib.System.IO.Base.html +++ b/Stdlib.System.IO.Base.html @@ -1,4 +1,4 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.System.IO.Base

Definitions

builtin IO +Juvix Documentation

stdlib - 0.0.1

Stdlib.System.IO.Base

Definitions

builtin IO axiom IO : TypeSource#

builtin IO-sequence -axiom >>> : IO -> IO -> IOSource#

\ No newline at end of file +axiom >>> : IO -> IO -> IOSource#

\ No newline at end of file diff --git a/Stdlib.System.IO.Bool-src.html b/Stdlib.System.IO.Bool-src.html index ba57eaf7..b294da47 100644 --- a/Stdlib.System.IO.Bool-src.html +++ b/Stdlib.System.IO.Bool-src.html @@ -1,5 +1,5 @@ -
module Stdlib.System.IO.Bool;
+
module Stdlib.System.IO.Bool;
 
 import Stdlib.System.IO.Base open;
 import Stdlib.Data.Bool open;
@@ -9,4 +9,4 @@
 axiom printBool : Bool -> IO;
 
 printBoolLn (b : Bool) : IO := printBool b >>> printString "\n";
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.System.IO.Bool.html b/Stdlib.System.IO.Bool.html index 6659f271..49c0070c 100644 --- a/Stdlib.System.IO.Bool.html +++ b/Stdlib.System.IO.Bool.html @@ -1,3 +1,3 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.System.IO.Bool

Definitions

builtin bool-print -axiom printBool : Bool -> IOSource#

printBoolLn (b : Bool) : IOSource#

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

Stdlib.System.IO.Bool

Definitions

builtin bool-print +axiom printBool : Bool -> IOSource#

printBoolLn (b : Bool) : IOSource#

\ No newline at end of file diff --git a/Stdlib.System.IO.Int-src.html b/Stdlib.System.IO.Int-src.html index 199684f5..f5b2e197 100644 --- a/Stdlib.System.IO.Int-src.html +++ b/Stdlib.System.IO.Int-src.html @@ -1,5 +1,5 @@ -
module Stdlib.System.IO.Int;
+
module Stdlib.System.IO.Int;
 
 import Stdlib.System.IO.Base open;
 import Stdlib.Data.Int open using {Int};
@@ -9,4 +9,4 @@
 axiom printInt : Int -> IO;
 
 printIntLn (i : Int) : IO := printInt i >>> printString "\n";
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.System.IO.Int.html b/Stdlib.System.IO.Int.html index 28e95ce0..d7276b38 100644 --- a/Stdlib.System.IO.Int.html +++ b/Stdlib.System.IO.Int.html @@ -1,3 +1,3 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.System.IO.Int

Definitions

builtin int-print -axiom printInt : Int -> IOSource#

printIntLn (i : Int) : IOSource#

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

Stdlib.System.IO.Int

Definitions

builtin int-print +axiom printInt : Int -> IOSource#

printIntLn (i : Int) : IOSource#

\ No newline at end of file diff --git a/Stdlib.System.IO.Nat-src.html b/Stdlib.System.IO.Nat-src.html index fa3d096e..313cf1a4 100644 --- a/Stdlib.System.IO.Nat-src.html +++ b/Stdlib.System.IO.Nat-src.html @@ -1,5 +1,5 @@ -
module Stdlib.System.IO.Nat;
+
module Stdlib.System.IO.Nat;
 
 import Stdlib.System.IO.Base open;
 import Stdlib.Data.Nat open;
@@ -9,4 +9,4 @@
 axiom printNat : Nat -> IO;
 
 printNatLn (n : Nat) : IO := printNat n >>> printString "\n";
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.System.IO.Nat.html b/Stdlib.System.IO.Nat.html index 99bb19d1..1df7400c 100644 --- a/Stdlib.System.IO.Nat.html +++ b/Stdlib.System.IO.Nat.html @@ -1,3 +1,3 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.System.IO.Nat

Definitions

builtin nat-print -axiom printNat : Nat -> IOSource#

printNatLn (n : Nat) : IOSource#

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

Stdlib.System.IO.Nat

Definitions

builtin nat-print +axiom printNat : Nat -> IOSource#

printNatLn (n : Nat) : IOSource#

\ No newline at end of file diff --git a/Stdlib.System.IO.String-src.html b/Stdlib.System.IO.String-src.html index c7eff587..9599ab4e 100644 --- a/Stdlib.System.IO.String-src.html +++ b/Stdlib.System.IO.String-src.html @@ -1,5 +1,5 @@ -
module Stdlib.System.IO.String;
+
module Stdlib.System.IO.String;
 
 import Stdlib.System.IO.Base open;
 import Stdlib.Data.String open;
@@ -11,4 +11,4 @@
 axiom readLn : (String -> IO) -> IO;
 
 printStringLn (s : String) : IO := printString s >>> printString "\n";
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.System.IO.String.html b/Stdlib.System.IO.String.html index b2b4c790..e7b8a74a 100644 --- a/Stdlib.System.IO.String.html +++ b/Stdlib.System.IO.String.html @@ -1,4 +1,4 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.System.IO.String

Definitions

builtin string-print +Juvix Documentation

stdlib - 0.0.1

Stdlib.System.IO.String

Definitions

builtin string-print axiom printString : String -> IOSource#

builtin IO-readline -axiom readLn : (String -> IO) -> IOSource#

printStringLn (s : String) : IOSource#

\ No newline at end of file +axiom readLn : (String -> IO) -> IOSource#

printStringLn (s : String) : IOSource#

\ No newline at end of file diff --git a/Stdlib.System.IO.html b/Stdlib.System.IO.html index ad7fdef6..160e0972 100644 --- a/Stdlib.System.IO.html +++ b/Stdlib.System.IO.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.System.IO

Definitions

import Stdlib.System.IO.Base open public

import Stdlib.System.IO.Bool open public

import Stdlib.System.IO.Nat open public

import Stdlib.System.IO.Int open public

import Stdlib.System.IO.String open public

print {A} {{Show A}} (a : A) : IOSource#

printLn {A} {{Show A}} (a : A) : IOSource#

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

Stdlib.System.IO

Definitions

import Stdlib.System.IO.Base open public

import Stdlib.System.IO.Bool open public

import Stdlib.System.IO.Nat open public

import Stdlib.System.IO.Int open public

import Stdlib.System.IO.String open public

print {A} {{Show A}} (a : A) : IOSource#

printLn {A} {{Show A}} (a : A) : IOSource#

\ No newline at end of file diff --git a/Stdlib.Trait-src.html b/Stdlib.Trait-src.html index ea690393..4d5acf70 100644 --- a/Stdlib.Trait-src.html +++ b/Stdlib.Trait-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Trait;
+
module Stdlib.Trait;
 
 import Stdlib.Trait.Eq as Eq open using {Eq; module Eq} public;
 import Stdlib.Trait.Show as Show open using {Show; module Show} public;
@@ -14,4 +14,4 @@
 import Stdlib.Trait.Integral open public;
 import Stdlib.Trait.Numeric open public;
 import Stdlib.Trait.DivMod open public;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Trait.Applicative-src.html b/Stdlib.Trait.Applicative-src.html index 2cbb4668..3b7a208e 100644 --- a/Stdlib.Trait.Applicative-src.html +++ b/Stdlib.Trait.Applicative-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Trait.Applicative;
+
module Stdlib.Trait.Applicative;
 
 import Stdlib.Data.Fixity open;
 import Stdlib.Function open;
@@ -15,49 +15,49 @@
 type Applicative (F : Type -> Type) :=
   mkApplicative@{
     {{functor}} : Functor F;
-    pure : {A : Type} -> A -> F A;
-    ap : {A B : Type} -> F (A -> B) -> F A -> F B;
+    pure : {A : Type} -> A -> F A;
+    ap : {A B : Type} -> F (A -> B) -> F A -> F B;
   };
 
-open Applicative public;
+open Applicative public;
 
 --- Sequences computations.
 --- Note that this function will be renamed to >>> once IO becomses a polymorphic type and can be given an Applicative instance.
-applicativeSeq
-  {F : Type -> Type}
-  {{Applicative F}}
-  {A B : Type}
-  (fa : F A)
-  (fb : F B)
-  : F B := ap (map λ{_ b := b} fa) fb;
+applicativeSeq
+  {F : Type -> Type}
+  {{Applicative F}}
+  {A B : Type}
+  (fa : F A)
+  (fb : F B)
+  : F B := ap (map λ{_ b := b} fa) fb;
 
 --- lifts a binary function to ;Applicative;
-liftA2
-  {F : Type -> Type}
-  {{Applicative F}}
-  {A B C}
-  (fun : A -> B -> C)
-  : F A -> F B -> F C := map fun >> ap;
+liftA2
+  {F : Type -> Type}
+  {{Applicative F}}
+  {A B C}
+  (fun : A -> B -> C)
+  : F A -> F B -> F C := map fun >> ap;
 
 syntax iterator mapA_ {init := 0; range := 1};
-mapA_
-  {t : Type -> Type}
-  {f : Type -> Type}
-  {A B}
-  {{Foldable t}}
-  {{Applicative f}}
-  (fun : A -> f B)
-  (l : t A)
-  : f Unit :=
-  rfor (acc := pure unit) (x in l) {
-    applicativeSeq (fun x) acc
+mapA_
+  {t : Type -> Type}
+  {f : Type -> Type}
+  {A B}
+  {{Foldable t}}
+  {{Applicative f}}
+  (fun : A -> f B)
+  (l : t A)
+  : f Unit :=
+  rfor (acc := pure unit) (x in l) {
+    applicativeSeq (fun x) acc
   };
-
-replicateA {F : Type -> Type} {A} {{Applicative F}} : Nat -> F A -> F (List A)
-  | zero _ := pure []
-  | (suc n) x := liftA2 (::) x (replicateA n x);
-
-when {F : Type -> Type} {{Applicative F}} : Bool -> F Unit -> F Unit
-  | false _ := pure unit
-  | true a := a;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
+replicateA {F : Type -> Type} {A} {{Applicative F}} : Nat -> F A -> F (List A)
+  | zero _ := pure []
+  | (suc n) x := liftA2 (::) x (replicateA n x);
+
+when {F : Type -> Type} {{Applicative F}} : Bool -> F Unit -> F Unit
+  | false _ := pure unit
+  | true a := a;
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Trait.Applicative.html b/Stdlib.Trait.Applicative.html index b4731727..a4750209 100644 --- a/Stdlib.Trait.Applicative.html +++ b/Stdlib.Trait.Applicative.html @@ -1,21 +1,21 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Applicative

Definitions

trait +Juvix Documentation

stdlib - 0.0.1

Stdlib.Trait.Applicative

Definitions

trait type Applicative (F : Type -> Type)Source#

Constructors

| mkApplicative@{ {{functor}} : Functor F; - pure : {A : Type} -> A -> F A; - ap : {A B : Type} -> F (A -> B) -> F A -> F B; - }

open Applicative public

applicativeSeq - {F : Type -> Type} {{Applicative F}} {A B : Type} (fa : F A) (fb : F B) : F BSource#

Sequences computations. Note that this function will be renamed to >>> once IO becomses a polymorphic type and can be given an Applicative instance.

liftA2 - {F : Type -> Type} - {{Applicative F}} - {A B C} - (fun : A -> B -> C) - : F A -> F B -> F CSource#

lifts a binary function to Applicative

mapA_ - {t : Type -> Type} - {f : Type -> Type} - {A B} - {{Foldable t}} - {{Applicative f}} - (fun : A -> f B) - (l : t A) - : f UnitSource#

replicateA {F : Type -> Type} {A} {{Applicative F}} : Nat -> F A -> F (List A)Source#

when {F : Type -> Type} {{Applicative F}} : Bool -> F Unit -> F UnitSource#

\ No newline at end of file + pure : {A : Type} -> A -> F A; + ap : {A B : Type} -> F (A -> B) -> F A -> F B; + }

open Applicative public

applicativeSeq + {F : Type -> Type} {{Applicative F}} {A B : Type} (fa : F A) (fb : F B) : F BSource#

Sequences computations. Note that this function will be renamed to >>> once IO becomses a polymorphic type and can be given an Applicative instance.

liftA2 + {F : Type -> Type} + {{Applicative F}} + {A B C} + (fun : A -> B -> C) + : F A -> F B -> F CSource#

lifts a binary function to Applicative

mapA_ + {t : Type -> Type} + {f : Type -> Type} + {A B} + {{Foldable t}} + {{Applicative f}} + (fun : A -> f B) + (l : t A) + : f UnitSource#

replicateA {F : Type -> Type} {A} {{Applicative F}} : Nat -> F A -> F (List A)Source#

when {F : Type -> Type} {{Applicative F}} : Bool -> F Unit -> F UnitSource#

\ No newline at end of file diff --git a/Stdlib.Trait.DivMod-src.html b/Stdlib.Trait.DivMod-src.html index 11c58a71..6741cc7a 100644 --- a/Stdlib.Trait.DivMod-src.html +++ b/Stdlib.Trait.DivMod-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Trait.DivMod;
+
module Stdlib.Trait.DivMod;
 
 trait
 type DivMod A :=
@@ -11,4 +11,4 @@
   };
 
 open DivMod public;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Trait.DivMod.html b/Stdlib.Trait.DivMod.html index 398583a6..8315cd45 100644 --- a/Stdlib.Trait.DivMod.html +++ b/Stdlib.Trait.DivMod.html @@ -1,8 +1,8 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.DivMod

Definitions

trait +Juvix Documentation

stdlib - 0.0.1

Stdlib.Trait.DivMod

Definitions

trait type DivMod ASource#

Constructors

| mkDivMod@{ {-# isabelle-operator: {name: "div", prec: 70, assoc: left} #-} div : A -> A -> A; {-# isabelle-operator: {name: "mod", prec: 70, assoc: left} #-} mod : A -> A -> A; - }

open DivMod public

\ No newline at end of file + }

open DivMod public

\ No newline at end of file diff --git a/Stdlib.Trait.Eq-src.html b/Stdlib.Trait.Eq-src.html index 4077e3dc..7b93c1f9 100644 --- a/Stdlib.Trait.Eq-src.html +++ b/Stdlib.Trait.Eq-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Trait.Eq;
+
module Stdlib.Trait.Eq;
 
 import Stdlib.Data.Bool.Base open;
 import Stdlib.Data.Fixity open;
@@ -17,4 +17,4 @@
 --- Test for inequality.
 {-# inline: always, isabelle-operator: {name: "\\<noteq>", prec: 50, assoc: none} #-}
 /= {A} {{Eq A}} (x y : A) : Bool := not (x == y);
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Trait.Eq.html b/Stdlib.Trait.Eq.html index cf48eb92..7aaf9a49 100644 --- a/Stdlib.Trait.Eq.html +++ b/Stdlib.Trait.Eq.html @@ -1,3 +1,3 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Eq

Definitions

trait -type Eq ASource#

A trait defining equality

Constructors

| mkEq@{eq : A -> A -> Bool}

== {A} {{Eq A}} : A -> A -> BoolSource#

/= {A} {{Eq A}} (x y : A) : BoolSource#

Test for inequality.

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

Stdlib.Trait.Eq

Definitions

trait +type Eq ASource#

A trait defining equality

Constructors

| mkEq@{eq : A -> A -> Bool}

== {A} {{Eq A}} : A -> A -> BoolSource#

/= {A} {{Eq A}} (x y : A) : BoolSource#

Test for inequality.

\ No newline at end of file diff --git a/Stdlib.Trait.Foldable-src.html b/Stdlib.Trait.Foldable-src.html index 1eb6b706..9692e8d5 100644 --- a/Stdlib.Trait.Foldable-src.html +++ b/Stdlib.Trait.Foldable-src.html @@ -1,6 +1,6 @@ -
module Stdlib.Trait.Foldable;
+
module Stdlib.Trait.Foldable;
 
 import Stdlib.Trait.Foldable.Polymorphic as Polymorphic public;
 import Stdlib.Trait.Foldable.Monomorphic open public;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Trait.Foldable.Monomorphic-src.html b/Stdlib.Trait.Foldable.Monomorphic-src.html index ef8eb9a3..ee3bba8f 100644 --- a/Stdlib.Trait.Foldable.Monomorphic-src.html +++ b/Stdlib.Trait.Foldable.Monomorphic-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Trait.Foldable.Monomorphic;
+
module Stdlib.Trait.Foldable.Monomorphic;
 
 import Stdlib.Function open;
 import Stdlib.Trait.Foldable.Polymorphic as Poly;
@@ -10,48 +10,48 @@
 type Foldable (Container Elem : Type) :=
   mkFoldable@{
     syntax iterator for {init := 1; range := 1};
-    for : {B : Type} -> (B -> Elem -> B) -> B -> Container -> B;
+    for : {B : Type} -> (B -> Elem -> B) -> B -> Container -> B;
 
     syntax iterator rfor {init := 1; range := 1};
-    rfor : {B : Type} -> (B -> Elem -> B) -> B -> Container -> B;
+    rfor : {B : Type} -> (B -> Elem -> B) -> B -> Container -> B;
   };
 
-open Foldable public;
+open Foldable public;
 
 --- 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.
 {-# inline: case #-}
-fromPolymorphicFoldable
-  {F : Type -> Type}
-  {{foldable : Poly.Foldable F}}
-  {Elem}
-  : Foldable (F Elem) Elem :=
+fromPolymorphicFoldable
+  {F : Type -> Type}
+  {{foldable : Poly.Foldable F}}
+  {Elem}
+  : Foldable (F Elem) Elem :=
   mkFoldable@{
-    for := Poly.for;
-    rfor := Poly.rfor;
+    for := Poly.for;
+    rfor := Poly.rfor;
   };
 
 {-# inline: true #-}
-foldl
-  {Container Elem}
-  {{Foldable Container Elem}}
-  {Acc : Type}
-  (fun : Acc -> Elem -> Acc)
-  (initialValue : Acc)
-  (container : Container)
-  : Acc :=
-  for (acc := initialValue) (x in container) {
-    fun acc x
+foldl
+  {Container Elem}
+  {{Foldable Container Elem}}
+  {Acc : Type}
+  (fun : Acc -> Elem -> Acc)
+  (initialValue : Acc)
+  (container : Container)
+  : Acc :=
+  for (acc := initialValue) (x in container) {
+    fun acc x
   };
 
 --- Combine the elements of the type using the provided function starting with the element in the right-most position.
 {-# inline: 2 #-}
-foldr
-  {Container Elem : Type}
-  {{Foldable Container Elem}}
-  {Acc : Type}
-  (fun : Elem -> Acc -> Acc)
-  (initialValue : Acc)
-  (container : Container)
-  : Acc := foldl (flip fun) initialValue container;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+foldr
+  {Container Elem : Type}
+  {{Foldable Container Elem}}
+  {Acc : Type}
+  (fun : Elem -> Acc -> Acc)
+  (initialValue : Acc)
+  (container : Container)
+  : Acc := foldl (flip fun) initialValue container;
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Trait.Foldable.Monomorphic.html b/Stdlib.Trait.Foldable.Monomorphic.html index d574a91c..e8987e5e 100644 --- a/Stdlib.Trait.Foldable.Monomorphic.html +++ b/Stdlib.Trait.Foldable.Monomorphic.html @@ -1,26 +1,26 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Foldable.Monomorphic

Definitions

trait +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}; - for : {B : Type} -> (B -> Elem -> B) -> B -> Container -> B; + for : {B : Type} -> (B -> Elem -> B) -> B -> Container -> B; syntax iterator rfor {init := 1; range := 1}; - rfor : {B : Type} -> (B -> Elem -> B) -> B -> Container -> B; - }

open Foldable public

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}} - {Acc : Type} - (fun : Acc -> Elem -> Acc) - (initialValue : Acc) - (container : Container) - : AccSource#

foldr - {Container Elem : Type} - {{Foldable Container Elem}} - {Acc : Type} - (fun : Elem -> Acc -> Acc) - (initialValue : Acc) - (container : Container) - : AccSource#

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 + rfor : {B : Type} -> (B -> Elem -> B) -> B -> Container -> B; + }

open Foldable public

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}} + {Acc : Type} + (fun : Acc -> Elem -> Acc) + (initialValue : Acc) + (container : Container) + : AccSource#

foldr + {Container Elem : Type} + {{Foldable Container Elem}} + {Acc : Type} + (fun : Elem -> Acc -> Acc) + (initialValue : Acc) + (container : Container) + : AccSource#

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 index 69d32444..2ad06cec 100644 --- a/Stdlib.Trait.Foldable.Polymorphic-src.html +++ b/Stdlib.Trait.Foldable.Polymorphic-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Trait.Foldable.Polymorphic;
+
module Stdlib.Trait.Foldable.Polymorphic;
 
 import Stdlib.Function open;
 
@@ -8,39 +8,39 @@
 type Foldable (F : Type -> Type) :=
   mkFoldable@{
     syntax iterator for {init := 1; range := 1};
-    for : {A B : Type} -> (B -> A -> B) -> B -> F A -> B;
+    for : {A B : Type} -> (B -> A -> B) -> B -> F A -> B;
 
     syntax iterator rfor {init := 1; range := 1};
-    rfor : {A B : Type} -> (B -> A -> B) -> B -> F A -> B;
+    rfor : {A B : Type} -> (B -> A -> B) -> B -> F A -> B;
   };
 
-open Foldable public;
+open Foldable public;
 
 --- Combine the elements of the type using the provided function starting with the element in the left-most position.
 {-# inline: true #-}
-foldl
-  {F : Type -> Type}
-  {{Foldable F}}
-  {Elem Acc : Type}
-  (fun : Acc -> Elem -> Acc)
-  (initialValue : Acc)
-  (container : F Elem)
-  : Acc :=
-  for (acc := initialValue) (x in container) {
-    fun acc x
+foldl
+  {F : Type -> Type}
+  {{Foldable F}}
+  {Elem Acc : Type}
+  (fun : Acc -> Elem -> Acc)
+  (initialValue : Acc)
+  (container : F Elem)
+  : Acc :=
+  for (acc := initialValue) (x in container) {
+    fun acc x
   };
 
 --- Combine the elements of the type using the provided function starting with the element in the right-most position.
 {-# inline: true #-}
-foldr
-  {F : Type -> Type}
-  {{Foldable F}}
-  {Elem Acc : Type}
-  (fun : Elem -> Acc -> Acc)
-  (initialValue : Acc)
-  (container : F Elem)
-  : Acc :=
-  rfor (acc := initialValue) (x in container) {
-    fun x acc
+foldr
+  {F : Type -> Type}
+  {{Foldable F}}
+  {Elem Acc : Type}
+  (fun : Elem -> Acc -> Acc)
+  (initialValue : Acc)
+  (container : F Elem)
+  : Acc :=
+  rfor (acc := initialValue) (x in container) {
+    fun x acc
   };
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Trait.Foldable.Polymorphic.html b/Stdlib.Trait.Foldable.Polymorphic.html index 06232671..011f2f2e 100644 --- a/Stdlib.Trait.Foldable.Polymorphic.html +++ b/Stdlib.Trait.Foldable.Polymorphic.html @@ -1,22 +1,22 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Foldable.Polymorphic

Definitions

trait +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}; - for : {A B : Type} -> (B -> A -> B) -> B -> F A -> B; + for : {A B : Type} -> (B -> A -> B) -> B -> F A -> B; syntax iterator rfor {init := 1; range := 1}; - rfor : {A B : Type} -> (B -> A -> B) -> B -> F A -> B; - }

open Foldable public

foldl - {F : Type -> Type} - {{Foldable F}} - {Elem Acc : Type} - (fun : Acc -> Elem -> Acc) - (initialValue : Acc) - (container : F Elem) - : AccSource#

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}} - {Elem Acc : Type} - (fun : Elem -> Acc -> Acc) - (initialValue : Acc) - (container : F Elem) - : AccSource#

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 + rfor : {A B : Type} -> (B -> A -> B) -> B -> F A -> B; + }

open Foldable public

foldl + {F : Type -> Type} + {{Foldable F}} + {Elem Acc : Type} + (fun : Acc -> Elem -> Acc) + (initialValue : Acc) + (container : F Elem) + : AccSource#

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}} + {Elem Acc : Type} + (fun : Elem -> Acc -> Acc) + (initialValue : Acc) + (container : F Elem) + : AccSource#

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 index 86996b8d..7a19fac5 100644 --- a/Stdlib.Trait.Foldable.html +++ b/Stdlib.Trait.Foldable.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Foldable

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

Stdlib.Trait.Foldable

\ No newline at end of file diff --git a/Stdlib.Trait.FromNatural-src.html b/Stdlib.Trait.FromNatural-src.html index 192daf4f..ab644d7c 100644 --- a/Stdlib.Trait.FromNatural-src.html +++ b/Stdlib.Trait.FromNatural-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Trait.FromNatural;
+
module Stdlib.Trait.FromNatural;
 
 import Juvix.Builtin.V1.Trait.FromNatural open public;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Trait.FromNatural.html b/Stdlib.Trait.FromNatural.html index cba959de..8239c053 100644 --- a/Stdlib.Trait.FromNatural.html +++ b/Stdlib.Trait.FromNatural.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.FromNatural

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

Stdlib.Trait.FromNatural

\ No newline at end of file diff --git a/Stdlib.Trait.Functor-src.html b/Stdlib.Trait.Functor-src.html index e4274966..668bb034 100644 --- a/Stdlib.Trait.Functor-src.html +++ b/Stdlib.Trait.Functor-src.html @@ -1,9 +1,9 @@ -
module Stdlib.Trait.Functor;
+
module Stdlib.Trait.Functor;
 
 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-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Trait.Functor.Monomorphic-src.html b/Stdlib.Trait.Functor.Monomorphic-src.html index 09ffedac..9d9a5c00 100644 --- a/Stdlib.Trait.Functor.Monomorphic-src.html +++ b/Stdlib.Trait.Functor.Monomorphic-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Trait.Functor.Monomorphic;
+
module Stdlib.Trait.Functor.Monomorphic;
 
 import Stdlib.Data.Fixity open;
 import Stdlib.Data.Unit open;
@@ -20,7 +20,7 @@
 fromPolymorphicFunctor
   {F : Type -> Type} {{Poly.Functor F}} {Elem} : Functor (F Elem) Elem :=
   mkFunctor@{
-    map := Poly.map;
+    map := Poly.map;
   };
 
 syntax operator <$> lapp;
@@ -40,4 +40,4 @@
   (container : Container)
   (element : Elem)
   : Container := \{_ := element} <$> container;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Trait.Functor.Monomorphic.html b/Stdlib.Trait.Functor.Monomorphic.html index e13058bd..a57d9cc9 100644 --- a/Stdlib.Trait.Functor.Monomorphic.html +++ b/Stdlib.Trait.Functor.Monomorphic.html @@ -1,5 +1,5 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Functor.Monomorphic

Definitions

trait +Juvix Documentation

stdlib - 0.0.1

Stdlib.Trait.Functor.Monomorphic

Definitions

trait type Functor (Container Elem : Type)Source#

Constructors

| mkFunctor@{ syntax iterator map {init := 0; range := 1}; {-# specialize: [1] #-} @@ -15,4 +15,4 @@ {{Functor Container Elem}} (container : Container) (element : Elem) - : ContainerSource#

\ No newline at end of file + : ContainerSource#

\ No newline at end of file diff --git a/Stdlib.Trait.Functor.Polymorphic-src.html b/Stdlib.Trait.Functor.Polymorphic-src.html index d8412a69..ba39eeed 100644 --- a/Stdlib.Trait.Functor.Polymorphic-src.html +++ b/Stdlib.Trait.Functor.Polymorphic-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Trait.Functor.Polymorphic;
+
module Stdlib.Trait.Functor.Polymorphic;
 
 import Stdlib.Data.Fixity open;
 import Stdlib.Data.Unit open;
@@ -10,22 +10,22 @@
   mkFunctor@{
     syntax iterator map {init := 0; range := 1};
     {-# specialize: [1] #-}
-    map : {A B : Type} -> (A -> B) -> F A -> F B;
+    map : {A B : Type} -> (A -> B) -> F A -> F B;
   };
 
-open Functor public;
+open Functor public;
 
 syntax operator <$> lapp;
 {-# inline: true #-}
-<$> {F : Type -> Type} {{Functor F}} {A B} (fun : A -> B) (fa : F A) : F B :=
-  map fun fa;
+<$> {F : Type -> Type} {{Functor F}} {A B} (fun : A -> B) (fa : F A) : F B :=
+  map fun fa;
 
 syntax operator $> lapp;
 {-# inline: true #-}
-$> {F : Type → Type} {A B : Type} {{Functor F}} (fa : F A) (b : B) : F B :=
-  λ{_ := b} <$> fa;
+$> {F : Type → Type} {A B : Type} {{Functor F}} (fa : F A) (b : B) : F B :=
+  λ{_ := b} <$> fa;
 
 {-# inline: true #-}
-void {F : Type → Type} {A : Type} {{Functor F}} (fa : F A) : F Unit :=
-  fa $> unit;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+void {F : Type → Type} {A : Type} {{Functor F}} (fa : F A) : F Unit :=
+  fa $> unit;
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Trait.Functor.Polymorphic.html b/Stdlib.Trait.Functor.Polymorphic.html index 8abf867b..bdd069e0 100644 --- a/Stdlib.Trait.Functor.Polymorphic.html +++ b/Stdlib.Trait.Functor.Polymorphic.html @@ -1,7 +1,7 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Functor.Polymorphic

Definitions

trait +Juvix Documentation

stdlib - 0.0.1

Stdlib.Trait.Functor.Polymorphic

Definitions

trait type Functor (F : Type -> Type)Source#

Constructors

| mkFunctor@{ syntax iterator map {init := 0; range := 1}; {-# specialize: [1] #-} - map : {A B : Type} -> (A -> B) -> F A -> F B; - }

open Functor public

<$> {F : Type -> Type} {{Functor F}} {A B} (fun : A -> B) (fa : F A) : F BSource#

$> {F : Type → Type} {A B : Type} {{Functor F}} (fa : F A) (b : B) : F BSource#

void {F : Type → Type} {A : Type} {{Functor F}} (fa : F A) : F UnitSource#

\ No newline at end of file + map : {A B : Type} -> (A -> B) -> F A -> F B; + }

open Functor public

<$> {F : Type -> Type} {{Functor F}} {A B} (fun : A -> B) (fa : F A) : F BSource#

$> {F : Type → Type} {A B : Type} {{Functor F}} (fa : F A) (b : B) : F BSource#

void {F : Type → Type} {A : Type} {{Functor F}} (fa : F A) : F UnitSource#

\ No newline at end of file diff --git a/Stdlib.Trait.Functor.html b/Stdlib.Trait.Functor.html index 5e328fd8..88d10ed8 100644 --- a/Stdlib.Trait.Functor.html +++ b/Stdlib.Trait.Functor.html @@ -1,4 +1,4 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Functor

Definitions

import Stdlib.Trait.Functor.Polymorphic open public

import Stdlib.Trait.Functor.Monomorphic as Monomorphic public

import Stdlib.Trait.Functor.Monomorphic open using { +Juvix Documentation

stdlib - 0.0.1

Stdlib.Trait.Functor

\ No newline at end of file +} public

\ No newline at end of file diff --git a/Stdlib.Trait.Integral-src.html b/Stdlib.Trait.Integral-src.html index a52c0797..9ea80ad5 100644 --- a/Stdlib.Trait.Integral-src.html +++ b/Stdlib.Trait.Integral-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Trait.Integral;
+
module Stdlib.Trait.Integral;
 
 import Stdlib.Data.Int.Base open using {Int};
 import Stdlib.Data.Fixity open;
@@ -17,4 +17,4 @@
   };
 
 open Integral using {fromInt; -} public;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Trait.Integral.html b/Stdlib.Trait.Integral.html index 43e8e69c..8e09c66e 100644 --- a/Stdlib.Trait.Integral.html +++ b/Stdlib.Trait.Integral.html @@ -1,5 +1,5 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Integral

Definitions

trait +Juvix Documentation

stdlib - 0.0.1

Stdlib.Trait.Integral

Definitions

trait type Integral ASource#

Constructors

| mkIntegral@{ naturalI : Natural A; syntax operator - additive; @@ -7,4 +7,4 @@ - : A -> A -> A; builtin from-int fromInt : Int -> A; - }

open Integral using {fromInt; -} public

\ No newline at end of file + }

open Integral using {fromInt; -} public

\ No newline at end of file diff --git a/Stdlib.Trait.Monad-src.html b/Stdlib.Trait.Monad-src.html index 7e92e1f8..8812d79f 100644 --- a/Stdlib.Trait.Monad-src.html +++ b/Stdlib.Trait.Monad-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Trait.Monad;
+
module Stdlib.Trait.Monad;
 
 import Stdlib.Data.Fixity open;
 import Stdlib.Trait.Applicative open;
@@ -9,22 +9,22 @@
   mkMonad@{
     {{applicative}} : Applicative M;
     builtin monad-bind
-    bind : {A B : Type} -> M A -> (A -> M B) -> M B;
+    bind : {A B : Type} -> M A -> (A -> M B) -> M B;
   };
 
-open Monad public;
+open Monad public;
 
 syntax operator >>= seq;
->>= {A B} {F : Type -> Type} {{Monad F}} (x : F A) (g : A -> F B) : F B :=
-  bind x g;
+>>= {A B} {F : Type -> Type} {{Monad F}} (x : F A) (g : A -> F B) : F B :=
+  bind x g;
 
 syntax operator >=> seq;
->=>
-  {A B C}
-  {F : Type -> Type}
-  {{Monad F}}
-  (h : A -> F B)
-  (g : B -> F C)
-  (a : A)
-  : F C := h a >>= g;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+>=>
+  {A B C}
+  {F : Type -> Type}
+  {{Monad F}}
+  (h : A -> F B)
+  (g : B -> F C)
+  (a : A)
+  : F C := h a >>= g;
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Trait.Monad.html b/Stdlib.Trait.Monad.html index 5998dfdd..68e5b0f8 100644 --- a/Stdlib.Trait.Monad.html +++ b/Stdlib.Trait.Monad.html @@ -1,14 +1,14 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Monad

Definitions

trait +Juvix Documentation

stdlib - 0.0.1

Stdlib.Trait.Monad

Definitions

trait type Monad (M : Type -> Type)Source#

Constructors

| mkMonad@{ {{applicative}} : Applicative M; builtin monad-bind - bind : {A B : Type} -> M A -> (A -> M B) -> M B; - }

open Monad public

>>= {A B} {F : Type -> Type} {{Monad F}} (x : F A) (g : A -> F B) : F BSource#

>=> - {A B C} - {F : Type -> Type} - {{Monad F}} - (h : A -> F B) - (g : B -> F C) - (a : A) - : F CSource#

\ No newline at end of file + bind : {A B : Type} -> M A -> (A -> M B) -> M B; + }

open Monad public

>>= {A B} {F : Type -> Type} {{Monad F}} (x : F A) (g : A -> F B) : F BSource#

>=> + {A B C} + {F : Type -> Type} + {{Monad F}} + (h : A -> F B) + (g : B -> F C) + (a : A) + : F CSource#

\ No newline at end of file diff --git a/Stdlib.Trait.Natural-src.html b/Stdlib.Trait.Natural-src.html index 794888ee..64fa466f 100644 --- a/Stdlib.Trait.Natural-src.html +++ b/Stdlib.Trait.Natural-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Trait.Natural;
+
module Stdlib.Trait.Natural;
 
 import Juvix.Builtin.V1.Trait.Natural open public;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Trait.Natural.html b/Stdlib.Trait.Natural.html index 928ef3eb..59fc26ff 100644 --- a/Stdlib.Trait.Natural.html +++ b/Stdlib.Trait.Natural.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Natural

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

Stdlib.Trait.Natural

\ No newline at end of file diff --git a/Stdlib.Trait.Numeric-src.html b/Stdlib.Trait.Numeric-src.html index a2d7b669..453433e1 100644 --- a/Stdlib.Trait.Numeric-src.html +++ b/Stdlib.Trait.Numeric-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Trait.Numeric;
+
module Stdlib.Trait.Numeric;
 
 import Stdlib.Data.Fixity open;
 import Stdlib.Trait.Integral open;
@@ -13,4 +13,4 @@
   };
 
 open Numeric using {/} public;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
Last modified on 2024-11-25 3:39 UTC
\ No newline at end of file diff --git a/Stdlib.Trait.Numeric.html b/Stdlib.Trait.Numeric.html index f4b4424d..41539d95 100644 --- a/Stdlib.Trait.Numeric.html +++ b/Stdlib.Trait.Numeric.html @@ -1,7 +1,7 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Numeric

Definitions

trait +Juvix Documentation

stdlib - 0.0.1

Stdlib.Trait.Numeric

Definitions

trait type Numeric ASource#

Constructors

| mkNumeric@{ integralI : Integral A; syntax operator / multiplicative; / : A -> A -> A; - }

open Numeric using {/} public

\ No newline at end of file + }

open Numeric using {/} public

\ No newline at end of file diff --git a/Stdlib.Trait.Ord-src.html b/Stdlib.Trait.Ord-src.html index 8b60f8dd..32c6a475 100644 --- a/Stdlib.Trait.Ord-src.html +++ b/Stdlib.Trait.Ord-src.html @@ -1,5 +1,5 @@ -
module Stdlib.Trait.Ord;
+
module Stdlib.Trait.Ord;
 
 import Stdlib.Data.Fixity open;
 import Stdlib.Data.Bool.Base open;
@@ -84,4 +84,4 @@
   if 
     | x > y := x
     | else := y;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
\ No newline at end of file diff --git a/Stdlib.Trait.Ord.html b/Stdlib.Trait.Ord.html index a8d17dc6..3e782044 100644 --- a/Stdlib.Trait.Ord.html +++ b/Stdlib.Trait.Ord.html @@ -1,4 +1,4 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Ord

Definitions

type OrderingSource#

Constructors

| LessThan
| Equal
| GreaterThan

isLessThan (ordering : Ordering) : BoolSource#

isEqual (ordering : Ordering) : BoolSource#

isGreaterThan (ordering : Ordering) : BoolSource#

instance +Juvix Documentation

stdlib - 0.0.1

Stdlib.Trait.Ord

Definitions

type OrderingSource#

Constructors

| LessThan
| Equal
| GreaterThan

isLessThan (ordering : Ordering) : BoolSource#

isEqual (ordering : Ordering) : BoolSource#

isGreaterThan (ordering : Ordering) : BoolSource#

instance orderingEqI : Eq OrderingSource#

trait -type Ord ASource#

A trait for defining a total order

Constructors

| mkOrd@{cmp : A -> A -> Ordering}

<= {A} {{Ord A}} (x y : A) : BoolSource#

Returns true iff the first element is less than or equal to the second.

< {A} {{Ord A}} (x y : A) : BoolSource#

Returns true iff the first element is less than the second.

> {A} {{Ord A}} (x y : A) : BoolSource#

Returns true iff the first element is greater than the second.

>= {A} {{Ord A}} (x y : A) : BoolSource#

Returns true iff the first element is greater than or equal to the second.

min {A} {{Ord A}} (x y : A) : ASource#

Returns the smaller element.

max {A} {{Ord A}} (x y : A) : ASource#

Returns the larger element.

\ No newline at end of file +type Ord ASource#

A trait for defining a total order

Constructors

| mkOrd@{cmp : A -> A -> Ordering}

<= {A} {{Ord A}} (x y : A) : BoolSource#

Returns true iff the first element is less than or equal to the second.

< {A} {{Ord A}} (x y : A) : BoolSource#

Returns true iff the first element is less than the second.

> {A} {{Ord A}} (x y : A) : BoolSource#

Returns true iff the first element is greater than the second.

>= {A} {{Ord A}} (x y : A) : BoolSource#

Returns true iff the first element is greater than or equal to the second.

min {A} {{Ord A}} (x y : A) : ASource#

Returns the smaller element.

max {A} {{Ord A}} (x y : A) : ASource#

Returns the larger element.

\ No newline at end of file diff --git a/Stdlib.Trait.Partial-src.html b/Stdlib.Trait.Partial-src.html index e9a305fe..2d10c3a8 100644 --- a/Stdlib.Trait.Partial-src.html +++ b/Stdlib.Trait.Partial-src.html @@ -1,13 +1,13 @@ -
module Stdlib.Trait.Partial;
+
module Stdlib.Trait.Partial;
 
 import Stdlib.Data.String.Base open;
 import Stdlib.Debug.Fail as Debug;
 
 trait
-type Partial := mkPartial@{fail : {A : Type} -> String -> A};
+type Partial := mkPartial@{fail : {A : Type} -> String -> A};
 
-open Partial public;
-
-runPartial {A} (f : {{Partial}} -> A) : A := f {{mkPartial Debug.failwith}};
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+open Partial public;
+
+runPartial {A} (f : {{Partial}} -> A) : A := f {{mkPartial Debug.failwith}};
+
\ No newline at end of file diff --git a/Stdlib.Trait.Partial.html b/Stdlib.Trait.Partial.html index 58a684a6..3ca990e3 100644 --- a/Stdlib.Trait.Partial.html +++ b/Stdlib.Trait.Partial.html @@ -1,3 +1,3 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Partial

Definitions

trait -type PartialSource#

Constructors

| mkPartial@{fail : {A : Type} -> String -> A}

open Partial public

runPartial {A} (f : {{Partial}} -> A) : ASource#

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

Stdlib.Trait.Partial

Definitions

trait +type PartialSource#

Constructors

| mkPartial@{fail : {A : Type} -> String -> A}

open Partial public

runPartial {A} (f : {{Partial}} -> A) : ASource#

\ No newline at end of file diff --git a/Stdlib.Trait.Show-src.html b/Stdlib.Trait.Show-src.html index e5b7e66b..51beff33 100644 --- a/Stdlib.Trait.Show-src.html +++ b/Stdlib.Trait.Show-src.html @@ -1,8 +1,8 @@ -
module Stdlib.Trait.Show;
+
module Stdlib.Trait.Show;
 
 import Stdlib.Data.String.Base open;
 
 trait
 type Show A := mkShow@{show : A -> String};
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
\ No newline at end of file diff --git a/Stdlib.Trait.Show.html b/Stdlib.Trait.Show.html index d8a5689a..a2bcaef1 100644 --- a/Stdlib.Trait.Show.html +++ b/Stdlib.Trait.Show.html @@ -1,3 +1,3 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Show

Definitions

trait -type Show ASource#

Constructors

| mkShow@{show : A -> String}
\ No newline at end of file +Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Show

Definitions

trait +type Show ASource#

Constructors

| mkShow@{show : A -> String}
\ No newline at end of file diff --git a/Stdlib.Trait.html b/Stdlib.Trait.html index d2d77a9b..ff806465 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.Applicative open public

import Stdlib.Trait.Monad open public

import Stdlib.Trait.Foldable open public

import Stdlib.Trait.Partial open public

import Stdlib.Trait.Natural open public

import Stdlib.Trait.FromNatural 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.Applicative open public

import Stdlib.Trait.Monad open public

import Stdlib.Trait.Foldable open public

import Stdlib.Trait.Partial open public

import Stdlib.Trait.Natural open public

import Stdlib.Trait.FromNatural 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/assets/css/latte-light.css b/assets/css/latte-light.css new file mode 100644 index 00000000..b7581fd5 --- /dev/null +++ b/assets/css/latte-light.css @@ -0,0 +1,30 @@ +/* Lighter version of the latte color palette based on https://github.com/catppuccin/catppuccin#-palette */ + +:root { + --ctp-rosewater: #dc8a78; + --ctp-flamingo: #dd7878; + --ctp-pink: #ea76cb; + --ctp-mauve: #8839ef; + --ctp-red: #d20f39; + --ctp-maroon: #e64553; + --ctp-peach: #fe640b; + --ctp-yellow: #df8e1d; + --ctp-green: #40a02b; + --ctp-teal: #179299; + --ctp-sky: #04a5e5; + --ctp-sapphire: #209fb5; + --ctp-blue: #1e66f5; + --ctp-lavender: #7287fd; + --ctp-text: #4c4f69; + --ctp-subtext1: #5c5f77; + --ctp-subtext0: #6c6f85; + --ctp-overlay2: #7c7f93; + --ctp-overlay1: #8c8fa1; + --ctp-overlay0: #9ca0b0; + --ctp-surface2: #acb0be; + --ctp-surface1: #bcc0cc; + --ctp-surface0: #ccd0da; + --ctp-base: #fbfcff; + --ctp-mantle: #f0f3f9; + --ctp-crust: #dce0e8; +} diff --git a/index-src.html b/index-src.html index 2a15a0f2..c32d6f03 100644 --- a/index-src.html +++ b/index-src.html @@ -1,5 +1,5 @@ -
{-
+
{-
 
 The Juvix standard library
 ------------------------------
@@ -26,4 +26,4 @@
 import Stdlib.Debug;
 
 import Stdlib.Extra.Gcd;
-
Last modified on 2024-11-18 3:38 UTC

\ No newline at end of file
+
\ No newline at end of file diff --git a/index.html b/index.html index be37f1e1..77315a3e 100644 --- a/index.html +++ b/index.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Modules

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

Modules

\ No newline at end of file