diff --git a/Juvix.Builtin.V1.Bool-src.html b/Juvix.Builtin.V1.Bool-src.html index ec3a8c34..3c998d25 100644 --- a/Juvix.Builtin.V1.Bool-src.html +++ b/Juvix.Builtin.V1.Bool-src.html @@ -6,4 +6,4 @@ type Bool := | true | false; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Juvix.Builtin.V1.Bool.html b/Juvix.Builtin.V1.Bool.html index 6d54ce72..9663e659 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

Description

Definitions

builtin bool -type BoolSource#

Inductive definition of booleans.

Constructors

| true
| false
\ No newline at end of file +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 a08e3911..1ec09bac 100644 --- a/Juvix.Builtin.V1.Fixity-src.html +++ b/Juvix.Builtin.V1.Fixity-src.html @@ -23,4 +23,4 @@ syntax fixity composition := binary {assoc := right; above := [multiplicative]}; syntax fixity lcomposition := binary {assoc := left; above := [multiplicative]}; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Juvix.Builtin.V1.Fixity.html b/Juvix.Builtin.V1.Fixity.html index b331eb62..2fce1c8f 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

Description

Definitions

syntax fixity noneSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 3}, _locCol = Pos {_unPos = 23}, _locOffset = Pos {_unPos = 55}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 3}, _locCol = Pos {_unPos = 27}, _locOffset = Pos {_unPos = 59}}}, _withLocParam = None}

syntax fixity rappSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 5}, _locCol = Pos {_unPos = 23}, _locOffset = Pos {_unPos = 84}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 5}, _locCol = Pos {_unPos = 30}, _locOffset = Pos {_unPos = 91}}}, _withLocParam = Binary}, right-associative

syntax fixity lappSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 6}, _locCol = Pos {_unPos = 23}, _locOffset = Pos {_unPos = 131}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 6}, _locCol = Pos {_unPos = 30}, _locOffset = Pos {_unPos = 138}}}, _withLocParam = Binary}, left-associative
Same precedence as rapp

syntax fixity seqSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 7}, _locCol = Pos {_unPos = 22}, _locOffset = Pos {_unPos = 190}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 7}, _locCol = Pos {_unPos = 29}, _locOffset = Pos {_unPos = 197}}}, _withLocParam = Binary}, left-associative
Higher precedence than: lapp,

syntax fixity functorSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 9}, _locCol = Pos {_unPos = 26}, _locOffset = Pos {_unPos = 257}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 9}, _locCol = Pos {_unPos = 33}, _locOffset = Pos {_unPos = 264}}}, _withLocParam = Binary}, right-associative

syntax fixity logicalSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 11}, _locCol = Pos {_unPos = 26}, _locOffset = Pos {_unPos = 308}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 11}, _locCol = Pos {_unPos = 33}, _locOffset = Pos {_unPos = 315}}}, _withLocParam = Binary}, right-associative
Higher precedence than: seq,

syntax fixity comparisonSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 12}, _locCol = Pos {_unPos = 29}, _locOffset = Pos {_unPos = 377}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 12}, _locCol = Pos {_unPos = 36}, _locOffset = Pos {_unPos = 384}}}, _withLocParam = Binary}
Higher precedence than: logical,

syntax fixity pairSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 14}, _locCol = Pos {_unPos = 23}, _locOffset = Pos {_unPos = 444}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 14}, _locCol = Pos {_unPos = 30}, _locOffset = Pos {_unPos = 451}}}, _withLocParam = Binary}, right-associative

syntax fixity consSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 15}, _locCol = Pos {_unPos = 23}, _locOffset = Pos {_unPos = 491}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 15}, _locCol = Pos {_unPos = 30}, _locOffset = Pos {_unPos = 498}}}, _withLocParam = Binary}, right-associative
Higher precedence than: pair,

syntax fixity stepSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 17}, _locCol = Pos {_unPos = 23}, _locOffset = Pos {_unPos = 556}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 17}, _locCol = Pos {_unPos = 30}, _locOffset = Pos {_unPos = 563}}}, _withLocParam = Binary}, right-associative

syntax fixity rangeSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 18}, _locCol = Pos {_unPos = 24}, _locOffset = Pos {_unPos = 604}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 18}, _locCol = Pos {_unPos = 31}, _locOffset = Pos {_unPos = 611}}}, _withLocParam = Binary}, right-associative
Higher precedence than: step,

syntax fixity additiveSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 20}, _locCol = Pos {_unPos = 27}, _locOffset = Pos {_unPos = 673}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 20}, _locCol = Pos {_unPos = 34}, _locOffset = Pos {_unPos = 680}}}, _withLocParam = Binary}, left-associative
Higher precedence than: comparison, range, cons,

syntax fixity multiplicativeSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 21}, _locCol = Pos {_unPos = 33}, _locOffset = Pos {_unPos = 765}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 21}, _locCol = Pos {_unPos = 40}, _locOffset = Pos {_unPos = 772}}}, _withLocParam = Binary}, left-associative
Higher precedence than: additive,

syntax fixity compositionSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 23}, _locCol = Pos {_unPos = 30}, _locOffset = Pos {_unPos = 840}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 23}, _locCol = Pos {_unPos = 37}, _locOffset = Pos {_unPos = 847}}}, _withLocParam = Binary}, right-associative
Higher precedence than: multiplicative,

syntax fixity lcompositionSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 24}, _locCol = Pos {_unPos = 31}, _locOffset = Pos {_unPos = 922}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 24}, _locCol = Pos {_unPos = 38}, _locOffset = Pos {_unPos = 929}}}, _withLocParam = Binary}, left-associative
Higher precedence than: multiplicative,
\ No newline at end of file +Juvix Documentation
stdlib - 0.0.1

Juvix.Builtin.V1.Fixity

Description

Definitions

syntax fixity noneSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 3}, _locCol = Pos {_unPos = 23}, _locOffset = Pos {_unPos = 55}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 3}, _locCol = Pos {_unPos = 27}, _locOffset = Pos {_unPos = 59}}}, _withLocParam = None}

syntax fixity rappSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 5}, _locCol = Pos {_unPos = 23}, _locOffset = Pos {_unPos = 84}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 5}, _locCol = Pos {_unPos = 30}, _locOffset = Pos {_unPos = 91}}}, _withLocParam = Binary}, right-associative

syntax fixity lappSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 6}, _locCol = Pos {_unPos = 23}, _locOffset = Pos {_unPos = 131}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 6}, _locCol = Pos {_unPos = 30}, _locOffset = Pos {_unPos = 138}}}, _withLocParam = Binary}, left-associative
Same precedence as rapp

syntax fixity seqSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 7}, _locCol = Pos {_unPos = 22}, _locOffset = Pos {_unPos = 190}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 7}, _locCol = Pos {_unPos = 29}, _locOffset = Pos {_unPos = 197}}}, _withLocParam = Binary}, left-associative
Higher precedence than: lapp,

syntax fixity functorSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 9}, _locCol = Pos {_unPos = 26}, _locOffset = Pos {_unPos = 257}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 9}, _locCol = Pos {_unPos = 33}, _locOffset = Pos {_unPos = 264}}}, _withLocParam = Binary}, right-associative

syntax fixity logicalSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 11}, _locCol = Pos {_unPos = 26}, _locOffset = Pos {_unPos = 308}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 11}, _locCol = Pos {_unPos = 33}, _locOffset = Pos {_unPos = 315}}}, _withLocParam = Binary}, right-associative
Higher precedence than: seq,

syntax fixity comparisonSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 12}, _locCol = Pos {_unPos = 29}, _locOffset = Pos {_unPos = 377}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 12}, _locCol = Pos {_unPos = 36}, _locOffset = Pos {_unPos = 384}}}, _withLocParam = Binary}
Higher precedence than: logical,

syntax fixity pairSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 14}, _locCol = Pos {_unPos = 23}, _locOffset = Pos {_unPos = 444}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 14}, _locCol = Pos {_unPos = 30}, _locOffset = Pos {_unPos = 451}}}, _withLocParam = Binary}, right-associative

syntax fixity consSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 15}, _locCol = Pos {_unPos = 23}, _locOffset = Pos {_unPos = 491}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 15}, _locCol = Pos {_unPos = 30}, _locOffset = Pos {_unPos = 498}}}, _withLocParam = Binary}, right-associative
Higher precedence than: pair,

syntax fixity stepSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 17}, _locCol = Pos {_unPos = 23}, _locOffset = Pos {_unPos = 556}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 17}, _locCol = Pos {_unPos = 30}, _locOffset = Pos {_unPos = 563}}}, _withLocParam = Binary}, right-associative

syntax fixity rangeSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 18}, _locCol = Pos {_unPos = 24}, _locOffset = Pos {_unPos = 604}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 18}, _locCol = Pos {_unPos = 31}, _locOffset = Pos {_unPos = 611}}}, _withLocParam = Binary}, right-associative
Higher precedence than: step,

syntax fixity additiveSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 20}, _locCol = Pos {_unPos = 27}, _locOffset = Pos {_unPos = 673}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 20}, _locCol = Pos {_unPos = 34}, _locOffset = Pos {_unPos = 680}}}, _withLocParam = Binary}, left-associative
Higher precedence than: comparison, range, cons,

syntax fixity multiplicativeSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 21}, _locCol = Pos {_unPos = 33}, _locOffset = Pos {_unPos = 765}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 21}, _locCol = Pos {_unPos = 40}, _locOffset = Pos {_unPos = 772}}}, _withLocParam = Binary}, left-associative
Higher precedence than: additive,

syntax fixity compositionSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 23}, _locCol = Pos {_unPos = 30}, _locOffset = Pos {_unPos = 840}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 23}, _locCol = Pos {_unPos = 37}, _locOffset = Pos {_unPos = 847}}}, _withLocParam = Binary}, right-associative
Higher precedence than: multiplicative,

syntax fixity lcompositionSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.3/package-base/Juvix/Builtin/V1/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 24}, _locCol = Pos {_unPos = 31}, _locOffset = Pos {_unPos = 922}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 24}, _locCol = Pos {_unPos = 38}, _locOffset = Pos {_unPos = 929}}}, _withLocParam = 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 41e362cd..c88242a1 100644 --- a/Juvix.Builtin.V1.List-src.html +++ b/Juvix.Builtin.V1.List-src.html @@ -11,4 +11,4 @@ nil | --- An element followed by a list :: a (List a); -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Juvix.Builtin.V1.List.html b/Juvix.Builtin.V1.List.html index 9d804821..b0758b54 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

Description

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 +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 da79a957..65e64fcd 100644 --- a/Juvix.Builtin.V1.Maybe-src.html +++ b/Juvix.Builtin.V1.Maybe-src.html @@ -7,4 +7,4 @@ type Maybe A := | nothing | just A; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Juvix.Builtin.V1.Maybe.html b/Juvix.Builtin.V1.Maybe.html index 56b1f904..6220d588 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

Description

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 +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 7fdcc4ba..43964236 100644 --- a/Juvix.Builtin.V1.Nat-src.html +++ b/Juvix.Builtin.V1.Nat-src.html @@ -13,4 +13,4 @@ * := (Nat.*); fromNat (x : Nat) : Nat := x }; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Juvix.Builtin.V1.Nat.Base-src.html b/Juvix.Builtin.V1.Nat.Base-src.html index 515742f5..fcf5d322 100644 --- a/Juvix.Builtin.V1.Nat.Base-src.html +++ b/Juvix.Builtin.V1.Nat.Base-src.html @@ -46,4 +46,4 @@ --- Modulo for ;Nat;s. builtin nat-mod mod (n m : Nat) : Nat := sub n (div n m * m); -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Juvix.Builtin.V1.Nat.Base.html b/Juvix.Builtin.V1.Nat.Base.html index 3374e3e4..a7fcb713 100644 --- a/Juvix.Builtin.V1.Nat.Base.html +++ b/Juvix.Builtin.V1.Nat.Base.html @@ -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 54ad0f0d..0916b32a 100644 --- a/Juvix.Builtin.V1.Nat.html +++ b/Juvix.Builtin.V1.Nat.html @@ -1,3 +1,3 @@ Juvix Documentation
stdlib - 0.0.1

Juvix.Builtin.V1.Nat

Description

Definitions

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

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

instance -naturalNatI : Natural NatSource#

\ 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 e845eac1..d1d02447 100644 --- a/Juvix.Builtin.V1.String-src.html +++ b/Juvix.Builtin.V1.String-src.html @@ -11,4 +11,4 @@ --- Concatenation of two ;String;s. builtin string-concat axiom ++str : String -> String -> String; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Juvix.Builtin.V1.String.html b/Juvix.Builtin.V1.String.html index 6c85f469..448c9114 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

Description

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.Natural-src.html b/Juvix.Builtin.V1.Trait.Natural-src.html index f57bd827..af6d82f1 100644 --- a/Juvix.Builtin.V1.Trait.Natural-src.html +++ b/Juvix.Builtin.V1.Trait.Natural-src.html @@ -16,4 +16,4 @@ }; open Natural public; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Juvix.Builtin.V1.Trait.Natural.html b/Juvix.Builtin.V1.Trait.Natural.html index 4439d80d..15e21ee9 100644 --- a/Juvix.Builtin.V1.Trait.Natural.html +++ b/Juvix.Builtin.V1.Trait.Natural.html @@ -7,4 +7,4 @@ * : A -> A -> A; builtin from-nat fromNat : Nat -> A - }

open Natural public

\ No newline at end of file + }

open Natural public

\ No newline at end of file diff --git a/Stdlib.Cairo.Poseidon-src.html b/Stdlib.Cairo.Poseidon-src.html index b8ba234d..6bab8d58 100644 --- a/Stdlib.Cairo.Poseidon-src.html +++ b/Stdlib.Cairo.Poseidon-src.html @@ -40,4 +40,4 @@ (poseidonHash acc@PoseidonState{ s0 := s0 + x1; s1 := s1 + x2 }) xs; in PoseidonState.s0 (go (mkPoseidonState 0 0 0) lst); -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Cairo.Poseidon.html b/Stdlib.Cairo.Poseidon.html index 82c314ab..f8cb20fd 100644 --- a/Stdlib.Cairo.Poseidon.html +++ b/Stdlib.Cairo.Poseidon.html @@ -5,4 +5,4 @@ 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 (lst : 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 (lst : List Field) : FieldSource#

Hashes n elements and retrieves a single field element output.

\ No newline at end of file diff --git a/Stdlib.Data.Bool-src.html b/Stdlib.Data.Bool-src.html index d2ed430d..9fbd22d1 100644 --- a/Stdlib.Data.Bool-src.html +++ b/Stdlib.Data.Bool-src.html @@ -32,4 +32,4 @@ | true := "true" | false := "false" }; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Data.Bool.Base-src.html b/Stdlib.Data.Bool.Base-src.html index 06b67846..6f531930 100644 --- a/Stdlib.Data.Bool.Base-src.html +++ b/Stdlib.Data.Bool.Base-src.html @@ -36,4 +36,4 @@ --- Logical conjunction. and (a b : Bool) : Bool := a && b; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Data.Bool.Base.html b/Stdlib.Data.Bool.Base.html index 4f9e4420..055c0593 100644 --- a/Stdlib.Data.Bool.Base.html +++ b/Stdlib.Data.Bool.Base.html @@ -2,4 +2,4 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Bool.Base

Description

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.

\ No newline at end of file +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.

\ No newline at end of file diff --git a/Stdlib.Data.Bool.html b/Stdlib.Data.Bool.html index 977a3d4e..c12020c9 100644 --- a/Stdlib.Data.Bool.html +++ b/Stdlib.Data.Bool.html @@ -2,4 +2,4 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Bool

Description

Definitions

import Stdlib.Data.Bool.Base open public

instance boolEqI : Eq BoolSource#

instance boolOrdI : Ord BoolSource#

instance -showBoolI : Show BoolSource#

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

\ No newline at end of file diff --git a/Stdlib.Data.Field-src.html b/Stdlib.Data.Field-src.html index f63ecbd2..25f8b257 100644 --- a/Stdlib.Data.Field-src.html +++ b/Stdlib.Data.Field-src.html @@ -47,4 +47,4 @@ integralI := integralFieldI; / := (Field./) }; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Data.Field.Base-src.html b/Stdlib.Data.Field.Base-src.html index a67da4fe..27b598ef 100644 --- a/Stdlib.Data.Field.Base-src.html +++ b/Stdlib.Data.Field.Base-src.html @@ -43,4 +43,4 @@ fromNat (n : Nat) : Field := fromInt (ofNat n); toInt (f : Field) : Int := ofNat (toNat f); -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Data.Field.Base.html b/Stdlib.Data.Field.Base.html index 7e9492fe..e7bd395f 100644 --- a/Stdlib.Data.Field.Base.html +++ b/Stdlib.Data.Field.Base.html @@ -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 7884bccd..3b42d4c0 100644 --- a/Stdlib.Data.Field.html +++ b/Stdlib.Data.Field.html @@ -4,4 +4,4 @@ showFieldI : Show FieldSource#

instance naturalFieldI : Natural FieldSource#

instance integralFieldI : Integral FieldSource#

instance -numericFieldI : Numeric FieldSource#

\ 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 38216df5..5d211c0d 100644 --- a/Stdlib.Data.Fixity-src.html +++ b/Stdlib.Data.Fixity-src.html @@ -2,4 +2,4 @@ 
module Stdlib.Data.Fixity;
 
 import Juvix.Builtin.V1.Fixity open public;
-
Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Data.Fixity.html b/Stdlib.Data.Fixity.html index 2365f652..c6727d7d 100644 --- a/Stdlib.Data.Fixity.html +++ b/Stdlib.Data.Fixity.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Fixity

Description

Definitions

import Juvix.Builtin.V1.Fixity open public

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

Stdlib.Data.Fixity

Description

Definitions

import Juvix.Builtin.V1.Fixity open public

\ No newline at end of file diff --git a/Stdlib.Data.Int-src.html b/Stdlib.Data.Int-src.html index a5015d67..ff1647a5 100644 --- a/Stdlib.Data.Int-src.html +++ b/Stdlib.Data.Int-src.html @@ -58,4 +58,4 @@ div := Int.div; mod := Int.mod }; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Data.Int.Base-src.html b/Stdlib.Data.Int.Base-src.html index 9b5c865d..100d3db1 100644 --- a/Stdlib.Data.Int.Base-src.html +++ b/Stdlib.Data.Int.Base-src.html @@ -92,4 +92,4 @@ abs : Int -> Nat | (ofNat n) := n | (negSuc n) := suc n; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Data.Int.Base.html b/Stdlib.Data.Int.Base.html index 09502208..8e02bb4f 100644 --- a/Stdlib.Data.Int.Base.html +++ b/Stdlib.Data.Int.Base.html @@ -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 -> NatSource#

Absolute value

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

Modulo for Ints.

abs : 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 c7f92346..04e180f0 100644 --- a/Stdlib.Data.Int.Ord-src.html +++ b/Stdlib.Data.Int.Ord-src.html @@ -59,4 +59,4 @@ --- Returns the biggest ;Int;. max (x y : Int) : Int := ite (x > y) x y; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Data.Int.Ord.html b/Stdlib.Data.Int.Ord.html index 0a3d300e..0add46e4 100644 --- a/Stdlib.Data.Int.Ord.html +++ b/Stdlib.Data.Int.Ord.html @@ -2,4 +2,4 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Int.Ord

Description

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 be6ac9b6..4aad671b 100644 --- a/Stdlib.Data.Int.html +++ b/Stdlib.Data.Int.html @@ -6,4 +6,4 @@ showIntI : Show 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 912b7822..0279a956 100644 --- a/Stdlib.Data.List-src.html +++ b/Stdlib.Data.List-src.html @@ -50,4 +50,4 @@ | nil := "nil" | s := "(" ++str go s ++str ")" }; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Data.List.Base-src.html b/Stdlib.Data.List.Base-src.html index be7a7668..4d1e7c7c 100644 --- a/Stdlib.Data.List.Base-src.html +++ b/Stdlib.Data.List.Base-src.html @@ -227,4 +227,4 @@ | nil := nil | (xs :: nil) := map λ {x := x :: nil} xs | (xs :: xss) := zipWith (::) xs (transpose xss); -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Data.List.Base.html b/Stdlib.Data.List.Base.html index a4daca5b..cbb968db 100644 --- a/Stdlib.Data.List.Base.html +++ b/Stdlib.Data.List.Base.html @@ -1,4 +1,4 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.List.Base

Description

Definitions

import Juvix.Builtin.V1.List open public

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

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

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

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

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

Right-associative fold.

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

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

Left-associative and tail-recursive fold.

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

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

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

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

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

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

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

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

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

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

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

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

Takes the first n elements of a List.

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

Drops the first n elements of a List.

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

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

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

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

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

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

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

Concatenates two Lists.

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

𝒪(𝓃). Append an element.

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

Concatenates a List of Lists.

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

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

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

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

tail {A} : List A → List ASource#

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

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

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

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

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

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

null {A} : List A → BoolSource#

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\ No newline at end of file diff --git a/Stdlib.Data.List.html b/Stdlib.Data.List.html index 2fc88b85..1194173f 100644 --- a/Stdlib.Data.List.html +++ b/Stdlib.Data.List.html @@ -2,4 +2,4 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.List

Description

Definitions

import Stdlib.Data.List.Base open public

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

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

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

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

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

\ No newline at end of file +showListI {A} {{Show A}} : Show (List A)Source#

\ No newline at end of file diff --git a/Stdlib.Data.Maybe-src.html b/Stdlib.Data.Maybe-src.html index 13b047b2..2012c725 100644 --- a/Stdlib.Data.Maybe-src.html +++ b/Stdlib.Data.Maybe-src.html @@ -36,4 +36,4 @@ | nothing (just _) := LT | (just _) nothing := GT }; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Data.Maybe.Base-src.html b/Stdlib.Data.Maybe.Base-src.html index d7fbadd7..d485149d 100644 --- a/Stdlib.Data.Maybe.Base-src.html +++ b/Stdlib.Data.Maybe.Base-src.html @@ -15,4 +15,4 @@ maybe {A B} (b : B) (f : A → B) : Maybe A → B | nothing := b | (just a) := f a; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Data.Maybe.Base.html b/Stdlib.Data.Maybe.Base.html index f84dc747..31e7121f 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

Description

Definitions

import Juvix.Builtin.V1.Maybe open public

fromMaybe {A} (a : A) : Maybe A → ASource#

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

maybe {A B} (b : B) (f : A → B) : Maybe A → BSource#

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

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

Stdlib.Data.Maybe.Base

Description

Definitions

import Juvix.Builtin.V1.Maybe open public

fromMaybe {A} (a : A) : Maybe A → ASource#

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

maybe {A B} (b : B) (f : A → B) : Maybe A → BSource#

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

\ No newline at end of file diff --git a/Stdlib.Data.Maybe.html b/Stdlib.Data.Maybe.html index 51ceace2..3e967ee3 100644 --- a/Stdlib.Data.Maybe.html +++ b/Stdlib.Data.Maybe.html @@ -2,4 +2,4 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Maybe

Description

Definitions

import Stdlib.Data.Maybe.Base open public

instance eqMaybeI {A} {{Eq A}} : Eq (Maybe A)Source#

instance showMaybeI {A} {{Show A}} : Show (Maybe A)Source#

instance -ordMaybeI {A} {{Ord A}} : Ord (Maybe A)Source#

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

\ No newline at end of file diff --git a/Stdlib.Data.Nat-src.html b/Stdlib.Data.Nat-src.html index aa3bb329..38747f4c 100644 --- a/Stdlib.Data.Nat-src.html +++ b/Stdlib.Data.Nat-src.html @@ -42,4 +42,4 @@ div := Nat.div; mod := Nat.mod }; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Data.Nat.Base-src.html b/Stdlib.Data.Nat.Base-src.html index 7407628c..8e9513f4 100644 --- a/Stdlib.Data.Nat.Base-src.html +++ b/Stdlib.Data.Nat.Base-src.html @@ -2,4 +2,4 @@ 
module Stdlib.Data.Nat.Base;
 
 import Juvix.Builtin.V1.Nat.Base open public;
-
Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Data.Nat.Base.html b/Stdlib.Data.Nat.Base.html index 87eda56c..dddfa5dc 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

Description

Definitions

import Juvix.Builtin.V1.Nat.Base open public

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

Stdlib.Data.Nat.Base

Description

Definitions

import Juvix.Builtin.V1.Nat.Base open public

\ No newline at end of file diff --git a/Stdlib.Data.Nat.Ord-src.html b/Stdlib.Data.Nat.Ord-src.html index cb455fe2..68fbef28 100644 --- a/Stdlib.Data.Nat.Ord-src.html +++ b/Stdlib.Data.Nat.Ord-src.html @@ -60,4 +60,4 @@ --- Returns the larger ;Nat;. max (x y : Nat) : Nat := ite (x > y) x y; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Data.Nat.Ord.html b/Stdlib.Data.Nat.Ord.html index f056fd18..66628a79 100644 --- a/Stdlib.Data.Nat.Ord.html +++ b/Stdlib.Data.Nat.Ord.html @@ -2,4 +2,4 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Nat.Ord

Description

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 f420ea19..f44b6515 100644 --- a/Stdlib.Data.Nat.html +++ b/Stdlib.Data.Nat.html @@ -5,4 +5,4 @@ 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 0844380c..c679dd0b 100644 --- a/Stdlib.Data.Pair-src.html +++ b/Stdlib.Data.Pair-src.html @@ -29,4 +29,4 @@ | {{mkShow show-a}} {{mkShow show-b}} := mkShow λ {(a, b) := "(" ++str show-a a ++str " , " ++str show-b b ++str ")"}; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Data.Pair.Base-src.html b/Stdlib.Data.Pair.Base-src.html index cd44f561..1ed46e0c 100644 --- a/Stdlib.Data.Pair.Base-src.html +++ b/Stdlib.Data.Pair.Base-src.html @@ -38,4 +38,4 @@ --- Applies a function to both components. both {A B} (f : A → B) : Pair A A → Pair B B | (a, b) := f a, f b; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Data.Pair.Base.html b/Stdlib.Data.Pair.Base.html index 99e8550f..1f1f5140 100644 --- a/Stdlib.Data.Pair.Base.html +++ b/Stdlib.Data.Pair.Base.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Pair.Base

Description

Definitions

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} (f : A -> B -> C) : Pair A B -> CSource#

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

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

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

fst {A B} : Pair A B → ASource#

Projects the first component of a tuple.

snd {A B} : Pair A B → BSource#

Projects the second component of a tuple.

swap {A B} : Pair A B → Pair B ASource#

Swaps the components of a tuple.

first {A B A'} (f : A → A') : Pair A B → Pair A' BSource#

Applies a function to the first component.

second {A B B'} (f : B → B') : Pair A B → Pair A B'Source#

Applies a function to the second component.

both {A B} (f : A → B) : Pair A A → Pair B BSource#

Applies a function to both components.

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

Stdlib.Data.Pair.Base

Description

Definitions

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} (f : A -> B -> C) : Pair A B -> CSource#

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

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

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

fst {A B} : Pair A B → ASource#

Projects the first component of a tuple.

snd {A B} : Pair A B → BSource#

Projects the second component of a tuple.

swap {A B} : Pair A B → Pair B ASource#

Swaps the components of a tuple.

first {A B A'} (f : A → A') : Pair A B → Pair A' BSource#

Applies a function to the first component.

second {A B B'} (f : B → B') : Pair A B → Pair A B'Source#

Applies a function to the second component.

both {A B} (f : A → B) : Pair A A → Pair B BSource#

Applies a function to both components.

\ No newline at end of file diff --git a/Stdlib.Data.Pair.html b/Stdlib.Data.Pair.html index fd932801..127452b7 100644 --- a/Stdlib.Data.Pair.html +++ b/Stdlib.Data.Pair.html @@ -2,4 +2,4 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Pair

Description

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.Result-src.html b/Stdlib.Data.Result-src.html index fd8bb7f7..37d19840 100644 --- a/Stdlib.Data.Result-src.html +++ b/Stdlib.Data.Result-src.html @@ -25,4 +25,4 @@ | (ok b1) (ok b2) := b1 == b2 | _ _ := false }; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Data.Result.Base-src.html b/Stdlib.Data.Result.Base-src.html index 0f0eaf8e..08cd925f 100644 --- a/Stdlib.Data.Result.Base-src.html +++ b/Stdlib.Data.Result.Base-src.html @@ -53,4 +53,4 @@ maybeToResult {E A} (defaultError : E) : Maybe A -> Result E A | nothing := error defaultError | (just x) := ok x; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Data.Result.Base.html b/Stdlib.Data.Result.Base.html index f38e62bf..3cd8df1e 100644 --- a/Stdlib.Data.Result.Base.html +++ b/Stdlib.Data.Result.Base.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Result.Base

Description

Definitions

type Result E ASource#

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

Constructors

| error E
| ok A

handleResult {E A B} (onError : E -> B) (onOk : A -> B) : Result E A -> BSource#

Apply the onError function if the value is error or apply the onOk function if the value is ok.

mapError {A E1 E2} (f : E1 -> E2) : Result E1 A -> Result E2 ASource#

Apply a function to the error value of a Result.

mapOk {E A C} (f : A -> C) : Result E A -> Result E CSource#

Apply a function to the ok value of a Result.

isError {E A} : Result E A -> BoolSource#

Return true if the value is an error, otherwise false.

isOk {E A} : Result E A -> BoolSource#

Return true if the value is ok, otherwise false.

fromError {E A} (default : E) : Result E A -> ESource#

Return the contents of an error value, otherwise return a default.

fromOk {E A} (default : A) : Result E A -> ASource#

Return the contents of an ok value, otherwise return a default.

resultToMaybe {E A} : Result E A -> Maybe ASource#

Convert a Result to a Maybe. An error value becomes `nothing`.

maybeToResult {E A} (defaultError : E) : Maybe A -> Result E ASource#

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

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

Stdlib.Data.Result.Base

Description

Definitions

type Result E ASource#

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

Constructors

| error E
| ok A

handleResult {E A B} (onError : E -> B) (onOk : A -> B) : Result E A -> BSource#

Apply the onError function if the value is error or apply the onOk function if the value is ok.

mapError {A E1 E2} (f : E1 -> E2) : Result E1 A -> Result E2 ASource#

Apply a function to the error value of a Result.

mapOk {E A C} (f : A -> C) : Result E A -> Result E CSource#

Apply a function to the ok value of a Result.

isError {E A} : Result E A -> BoolSource#

Return true if the value is an error, otherwise false.

isOk {E A} : Result E A -> BoolSource#

Return true if the value is ok, otherwise false.

fromError {E A} (default : E) : Result E A -> ESource#

Return the contents of an error value, otherwise return a default.

fromOk {E A} (default : A) : Result E A -> ASource#

Return the contents of an ok value, otherwise return a default.

resultToMaybe {E A} : Result E A -> Maybe ASource#

Convert a Result to a Maybe. An error value becomes `nothing`.

maybeToResult {E A} (defaultError : E) : Maybe A -> Result E ASource#

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 688c5872..63e3f280 100644 --- a/Stdlib.Data.Result.html +++ b/Stdlib.Data.Result.html @@ -1,4 +1,4 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Result

Description

Definitions

import Stdlib.Data.Result.Base open public

instance ordResultI {A B} {{Ord A}} {{Ord B}} : Ord (Result A B)Source#

instance -eqResultI {A B} {{Eq A}} {{Eq B}} : Eq (Result A B)Source#

\ No newline at end of file +eqResultI {A B} {{Eq A}} {{Eq B}} : Eq (Result A B)Source#

\ No newline at end of file diff --git a/Stdlib.Data.String-src.html b/Stdlib.Data.String-src.html index e4f83b7b..5adb69d9 100644 --- a/Stdlib.Data.String-src.html +++ b/Stdlib.Data.String-src.html @@ -16,4 +16,4 @@ let go (s : String) : String := "\"" ++str s ++str "\""; in mkShow go; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Data.String.Base-src.html b/Stdlib.Data.String.Base-src.html index 8cfd5d03..3ee175e6 100644 --- a/Stdlib.Data.String.Base-src.html +++ b/Stdlib.Data.String.Base-src.html @@ -11,4 +11,4 @@ --- Joins a ;List; of ;String;s with "\n". unlines : List String -> String := intersperse "\n" >> concatStr; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Data.String.Base.html b/Stdlib.Data.String.Base.html index 3a2d8469..0e92289a 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

Description

Definitions

import Juvix.Builtin.V1.String open public

concatStr : List String -> StringSource#

Concatenates a List of Strings.

unlines : 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

Description

Definitions

import Juvix.Builtin.V1.String open public

concatStr : List String -> StringSource#

Concatenates a List of Strings.

unlines : 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 53a157da..ebd36ee3 100644 --- a/Stdlib.Data.String.Ord-src.html +++ b/Stdlib.Data.String.Ord-src.html @@ -10,4 +10,4 @@ --- Equality for ;String;s. builtin string-eq axiom == : String → String → Bool; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Data.String.Ord.html b/Stdlib.Data.String.Ord.html index 099f7c83..f7198529 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

Description

Definitions

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

Equality for Strings.

\ No newline at end of file +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 f3a29dce..b2e4d25b 100644 --- a/Stdlib.Data.String.html +++ b/Stdlib.Data.String.html @@ -1,4 +1,4 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.String

Description

Definitions

import Stdlib.Data.String.Base open public

instance eqStringI : Eq StringSource#

instance -showStringI : Show StringSource#

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

\ No newline at end of file diff --git a/Stdlib.Data.Unit-src.html b/Stdlib.Data.Unit-src.html index 72b4f08e..feafa1b5 100644 --- a/Stdlib.Data.Unit-src.html +++ b/Stdlib.Data.Unit-src.html @@ -20,4 +20,4 @@ instance showUnitI : Show Unit := mkShow λ {unit := "unit"}; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Data.Unit.html b/Stdlib.Data.Unit.html index c22f2217..d3b871d7 100644 --- a/Stdlib.Data.Unit.html +++ b/Stdlib.Data.Unit.html @@ -2,4 +2,4 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Unit

Description

The unit type.

Definitions

type UnitSource#

Constructors

| unit

The only constructor of Unit.

instance eqUnitI : Eq UnitSource#

instance ordUnitI : Ord UnitSource#

instance -showUnitI : Show UnitSource#

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

\ No newline at end of file diff --git a/Stdlib.Debug.Fail-src.html b/Stdlib.Debug.Fail-src.html index 3f9542f1..b360108f 100644 --- a/Stdlib.Debug.Fail-src.html +++ b/Stdlib.Debug.Fail-src.html @@ -6,4 +6,4 @@ --- Primitive that exits the program with an error message. builtin fail axiom failwith : {A : Type} → String → A; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Debug.Fail.html b/Stdlib.Debug.Fail.html index 1e5a2892..07d6c4c4 100644 --- a/Stdlib.Debug.Fail.html +++ b/Stdlib.Debug.Fail.html @@ -1,3 +1,3 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Debug.Fail

Description

Definitions

builtin fail -axiom failwith : {A : Type} → String → ASource#

Primitive that exits the program with an error message.

\ No newline at end of file +axiom failwith : {A : Type} → String → ASource#

Primitive that exits the program with an error message.

\ No newline at end of file diff --git a/Stdlib.Function-src.html b/Stdlib.Function-src.html index ab23aa5d..43eae190 100644 --- a/Stdlib.Function-src.html +++ b/Stdlib.Function-src.html @@ -55,4 +55,4 @@ builtin seq >-> : {A B : Type} → A → B → B | x y := y; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Function.html b/Stdlib.Function.html index 3b229af5..96319bf8 100644 --- a/Stdlib.Function.html +++ b/Stdlib.Function.html @@ -1,3 +1,3 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Function

Description

Definitions

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

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

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

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

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

Always returns the first argument.

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.

<| {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} : Nat -> (A -> A) -> A -> ASource#

Applies a function n times.

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

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

\ No newline at end of file +>-> : {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 66259568..497dfa04 100644 --- a/Stdlib.Prelude-src.html +++ b/Stdlib.Prelude-src.html @@ -18,4 +18,4 @@ import Stdlib.System.IO open public; import Stdlib.Trait open public; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Prelude.html b/Stdlib.Prelude.html index 8e73014c..5fb8b62b 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.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.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.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.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 e5e6ca39..4ab5fb75 100644 --- a/Stdlib.System.IO-src.html +++ b/Stdlib.System.IO-src.html @@ -12,4 +12,4 @@ print {A} {{Show A}} (a : A) : IO := printString (Show.show a); printLn {A} {{Show A}} (a : A) : IO := printStringLn (Show.show a); -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.System.IO.Base-src.html b/Stdlib.System.IO.Base-src.html index 6b9958c8..08190cd5 100644 --- a/Stdlib.System.IO.Base-src.html +++ b/Stdlib.System.IO.Base-src.html @@ -9,4 +9,4 @@ syntax operator >>> seq; builtin IO-sequence axiom >>> : IO → IO → IO; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.System.IO.Base.html b/Stdlib.System.IO.Base.html index c5360f86..f9871793 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

Description

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 deb3f36b..766f0697 100644 --- a/Stdlib.System.IO.Bool-src.html +++ b/Stdlib.System.IO.Bool-src.html @@ -9,4 +9,4 @@ axiom printBool : Bool → IO; printBoolLn (b : Bool) : IO := printBool b >>> printString "\n"; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.System.IO.Bool.html b/Stdlib.System.IO.Bool.html index f123284d..0f01c830 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

Description

Definitions

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

printBoolLn (b : Bool) : IOSource#

\ No newline at end of file +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 87dad019..f7a8269a 100644 --- a/Stdlib.System.IO.Int-src.html +++ b/Stdlib.System.IO.Int-src.html @@ -9,4 +9,4 @@ axiom printInt : Int → IO; printIntLn (i : Int) : IO := printInt i >>> printString "\n"; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.System.IO.Int.html b/Stdlib.System.IO.Int.html index 9a065f52..52c485c1 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

Description

Definitions

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

printIntLn (i : Int) : IOSource#

\ No newline at end of file +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 c9983483..401c02d8 100644 --- a/Stdlib.System.IO.Nat-src.html +++ b/Stdlib.System.IO.Nat-src.html @@ -9,4 +9,4 @@ axiom printNat : Nat → IO; printNatLn (n : Nat) : IO := printNat n >>> printString "\n"; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.System.IO.Nat.html b/Stdlib.System.IO.Nat.html index 8fc55ac9..ae3571d3 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

Description

Definitions

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

printNatLn (n : Nat) : IOSource#

\ No newline at end of file +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 0e687f8d..8e2bb92c 100644 --- a/Stdlib.System.IO.String-src.html +++ b/Stdlib.System.IO.String-src.html @@ -11,4 +11,4 @@ axiom readLn : (String → IO) → IO; printStringLn (s : String) : IO := printString s >>> printString "\n"; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.System.IO.String.html b/Stdlib.System.IO.String.html index 259cc378..6a3caebf 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

Description

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 48a64745..78e56c91 100644 --- a/Stdlib.System.IO.html +++ b/Stdlib.System.IO.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.System.IO

Description

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

Description

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 c0003714..cd2896bf 100644 --- a/Stdlib.Trait-src.html +++ b/Stdlib.Trait-src.html @@ -9,4 +9,4 @@ import Stdlib.Trait.Integral open public; import Stdlib.Trait.Numeric open public; import Stdlib.Trait.DivMod open public; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Trait.DivMod-src.html b/Stdlib.Trait.DivMod-src.html index d1133e95..2fc2b39b 100644 --- a/Stdlib.Trait.DivMod-src.html +++ b/Stdlib.Trait.DivMod-src.html @@ -9,4 +9,4 @@ }; open DivMod public; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Trait.DivMod.html b/Stdlib.Trait.DivMod.html index f217a525..b299b2c6 100644 --- a/Stdlib.Trait.DivMod.html +++ b/Stdlib.Trait.DivMod.html @@ -3,4 +3,4 @@ type DivMod ASource#

Constructors

| mkDivMod { div : A -> A -> A; 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 43348121..bd254f80 100644 --- a/Stdlib.Trait.Eq-src.html +++ b/Stdlib.Trait.Eq-src.html @@ -17,4 +17,4 @@ --- Tests for inequality. {-# inline: always #-} /= {A} {{Eq A}} (x y : A) : Bool := not (x == y); -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Eq.html b/Stdlib.Trait.Eq.html index 30a3395d..16596a67 100644 --- a/Stdlib.Trait.Eq.html +++ b/Stdlib.Trait.Eq.html @@ -1,3 +1,3 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Eq

Description

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#

Tests for inequality.

\ No newline at end of file +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#

Tests for inequality.

\ No newline at end of file diff --git a/Stdlib.Trait.Integral-src.html b/Stdlib.Trait.Integral-src.html index 82daf715..44cf8880 100644 --- a/Stdlib.Trait.Integral-src.html +++ b/Stdlib.Trait.Integral-src.html @@ -16,4 +16,4 @@ }; open Integral using {fromInt; -} public; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Integral.html b/Stdlib.Trait.Integral.html index 0741313b..5f01d0e1 100644 --- a/Stdlib.Trait.Integral.html +++ b/Stdlib.Trait.Integral.html @@ -6,4 +6,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.Natural-src.html b/Stdlib.Trait.Natural-src.html index b7f73a20..b7ab4037 100644 --- a/Stdlib.Trait.Natural-src.html +++ b/Stdlib.Trait.Natural-src.html @@ -2,4 +2,4 @@ 
module Stdlib.Trait.Natural;
 
 import Juvix.Builtin.V1.Trait.Natural open public;
-
Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Natural.html b/Stdlib.Trait.Natural.html index 08942aed..6c54b359 100644 --- a/Stdlib.Trait.Natural.html +++ b/Stdlib.Trait.Natural.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Natural

Description

Definitions

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

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

Stdlib.Trait.Natural

Description

Definitions

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

\ No newline at end of file diff --git a/Stdlib.Trait.Numeric-src.html b/Stdlib.Trait.Numeric-src.html index 1e2faf25..f32c5b83 100644 --- a/Stdlib.Trait.Numeric-src.html +++ b/Stdlib.Trait.Numeric-src.html @@ -13,4 +13,4 @@ }; open Numeric using {/} public; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Numeric.html b/Stdlib.Trait.Numeric.html index 646a5a8f..0e7aa448 100644 --- a/Stdlib.Trait.Numeric.html +++ b/Stdlib.Trait.Numeric.html @@ -4,4 +4,4 @@ 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 2ffa8294..551b843d 100644 --- a/Stdlib.Trait.Ord-src.html +++ b/Stdlib.Trait.Ord-src.html @@ -74,4 +74,4 @@ --- Returns the larger element. {-# inline: always #-} max {A} {{Ord A}} (x y : A) : A := ite (x > y) x y; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Ord.html b/Stdlib.Trait.Ord.html index 9bd3ddbd..5d7d751f 100644 --- a/Stdlib.Trait.Ord.html +++ b/Stdlib.Trait.Ord.html @@ -1,4 +1,4 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Ord

Description

Definitions

type OrderingSource#

Constructors

| LT : Ordering
| EQ : Ordering
| GT : Ordering

isLT : Ordering → BoolSource#

isEQ : Ordering → BoolSource#

isGT : 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 eee3f057..6950dfbe 100644 --- a/Stdlib.Trait.Partial-src.html +++ b/Stdlib.Trait.Partial-src.html @@ -10,4 +10,4 @@ open Partial public; runPartial {A} (f : {{Partial}} -> A) : A := f {{mkPartial Debug.failwith}}; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Partial.html b/Stdlib.Trait.Partial.html index 65916ebd..f89126d6 100644 --- a/Stdlib.Trait.Partial.html +++ b/Stdlib.Trait.Partial.html @@ -1,3 +1,3 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Partial

Description

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 +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 eb99fa1f..36d6ae76 100644 --- a/Stdlib.Trait.Show-src.html +++ b/Stdlib.Trait.Show-src.html @@ -5,4 +5,4 @@ trait type Show A := mkShow {show : A -> String}; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Show.html b/Stdlib.Trait.Show.html index e064fe33..8281faa3 100644 --- a/Stdlib.Trait.Show.html +++ b/Stdlib.Trait.Show.html @@ -1,3 +1,3 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Show

Description

Definitions

trait -type Show ASource#

Constructors

| mkShow {show : A -> String}
\ No newline at end of file +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 870877e7..f6d056f6 100644 --- a/Stdlib.Trait.html +++ b/Stdlib.Trait.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait

Description

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.Partial open public

import Stdlib.Trait.Natural open public

import Stdlib.Trait.Integral open public

import Stdlib.Trait.Numeric open public

import Stdlib.Trait.DivMod open public

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

Stdlib.Trait

Description

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.Partial open public

import Stdlib.Trait.Natural open public

import Stdlib.Trait.Integral open public

import Stdlib.Trait.Numeric open public

import Stdlib.Trait.DivMod open public

\ No newline at end of file diff --git a/index-src.html b/index-src.html index 05918f39..0355dfab 100644 --- a/index-src.html +++ b/index-src.html @@ -16,4 +16,4 @@ import Stdlib.Data.String.Ord; import Stdlib.Cairo.Poseidon; -Last modified on 2024-07-10 15:52 UTC \ No newline at end of file +Last modified on 2024-07-15 14:08 UTC \ No newline at end of file diff --git a/index.html b/index.html index b37ffcd6..9c8a4aeb 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