From 626c9dfc4814a285305da2acfe22b26cff4389db Mon Sep 17 00:00:00 2001 From: paulcadman Date: Wed, 10 Jul 2024 15:53:13 +0000 Subject: [PATCH] deploy: 216cb609cbe5aec9badea858f151a5ea400f2e66 --- Juvix.Builtin.V1.Bool-src.html | 2 +- Juvix.Builtin.V1.Bool.html | 2 +- Juvix.Builtin.V1.Fixity-src.html | 2 +- Juvix.Builtin.V1.Fixity.html | 2 +- Juvix.Builtin.V1.List-src.html | 2 +- Juvix.Builtin.V1.List.html | 2 +- Juvix.Builtin.V1.Maybe-src.html | 2 +- Juvix.Builtin.V1.Maybe.html | 2 +- Juvix.Builtin.V1.Nat-src.html | 2 +- Juvix.Builtin.V1.Nat.Base-src.html | 2 +- Juvix.Builtin.V1.Nat.Base.html | 2 +- Juvix.Builtin.V1.Nat.html | 2 +- Juvix.Builtin.V1.String-src.html | 2 +- Juvix.Builtin.V1.String.html | 2 +- Juvix.Builtin.V1.Trait.Natural-src.html | 2 +- Juvix.Builtin.V1.Trait.Natural.html | 2 +- Stdlib.Cairo.Poseidon-src.html | 2 +- Stdlib.Cairo.Poseidon.html | 2 +- Stdlib.Data.Bool-src.html | 2 +- Stdlib.Data.Bool.Base-src.html | 2 +- Stdlib.Data.Bool.Base.html | 2 +- Stdlib.Data.Bool.html | 2 +- Stdlib.Data.Field-src.html | 2 +- Stdlib.Data.Field.Base-src.html | 2 +- Stdlib.Data.Field.Base.html | 2 +- Stdlib.Data.Field.html | 2 +- Stdlib.Data.Fixity-src.html | 2 +- Stdlib.Data.Fixity.html | 2 +- Stdlib.Data.Int-src.html | 2 +- Stdlib.Data.Int.Base-src.html | 2 +- Stdlib.Data.Int.Base.html | 2 +- Stdlib.Data.Int.Ord-src.html | 2 +- Stdlib.Data.Int.Ord.html | 2 +- Stdlib.Data.Int.html | 2 +- Stdlib.Data.List-src.html | 2 +- Stdlib.Data.List.Base-src.html | 181 +++++++++++++----------- Stdlib.Data.List.Base.html | 6 +- Stdlib.Data.List.html | 2 +- Stdlib.Data.Maybe-src.html | 2 +- Stdlib.Data.Maybe.Base-src.html | 2 +- Stdlib.Data.Maybe.Base.html | 2 +- Stdlib.Data.Maybe.html | 2 +- Stdlib.Data.Nat-src.html | 2 +- Stdlib.Data.Nat.Base-src.html | 2 +- Stdlib.Data.Nat.Base.html | 2 +- Stdlib.Data.Nat.Ord-src.html | 2 +- Stdlib.Data.Nat.Ord.html | 2 +- Stdlib.Data.Nat.html | 2 +- Stdlib.Data.Pair-src.html | 2 +- Stdlib.Data.Pair.Base-src.html | 2 +- Stdlib.Data.Pair.Base.html | 2 +- Stdlib.Data.Pair.html | 2 +- Stdlib.Data.Result-src.html | 28 ++++ Stdlib.Data.Result.Base-src.html | 56 ++++++++ Stdlib.Data.Result.Base.html | 2 + Stdlib.Data.Result.html | 4 + Stdlib.Data.String-src.html | 2 +- Stdlib.Data.String.Base-src.html | 6 +- Stdlib.Data.String.Base.html | 2 +- Stdlib.Data.String.Ord-src.html | 2 +- Stdlib.Data.String.Ord.html | 2 +- Stdlib.Data.String.html | 2 +- Stdlib.Data.Unit-src.html | 2 +- Stdlib.Data.Unit.html | 2 +- Stdlib.Debug.Fail-src.html | 2 +- Stdlib.Debug.Fail.html | 2 +- Stdlib.Function-src.html | 2 +- Stdlib.Function.html | 2 +- Stdlib.Prelude-src.html | 3 +- Stdlib.Prelude.html | 2 +- Stdlib.System.IO-src.html | 2 +- Stdlib.System.IO.Base-src.html | 2 +- Stdlib.System.IO.Base.html | 2 +- Stdlib.System.IO.Bool-src.html | 2 +- Stdlib.System.IO.Bool.html | 2 +- Stdlib.System.IO.Int-src.html | 2 +- Stdlib.System.IO.Int.html | 2 +- Stdlib.System.IO.Nat-src.html | 2 +- Stdlib.System.IO.Nat.html | 2 +- Stdlib.System.IO.String-src.html | 2 +- Stdlib.System.IO.String.html | 2 +- Stdlib.System.IO.html | 2 +- Stdlib.Trait-src.html | 2 +- Stdlib.Trait.DivMod-src.html | 2 +- Stdlib.Trait.DivMod.html | 2 +- Stdlib.Trait.Eq-src.html | 2 +- Stdlib.Trait.Eq.html | 2 +- Stdlib.Trait.Integral-src.html | 2 +- Stdlib.Trait.Integral.html | 2 +- Stdlib.Trait.Natural-src.html | 2 +- Stdlib.Trait.Natural.html | 2 +- Stdlib.Trait.Numeric-src.html | 2 +- Stdlib.Trait.Numeric.html | 2 +- Stdlib.Trait.Ord-src.html | 2 +- Stdlib.Trait.Ord.html | 2 +- Stdlib.Trait.Partial-src.html | 2 +- Stdlib.Trait.Partial.html | 2 +- Stdlib.Trait.Show-src.html | 2 +- Stdlib.Trait.Show.html | 2 +- Stdlib.Trait.html | 2 +- index-src.html | 2 +- index.html | 2 +- 102 files changed, 287 insertions(+), 187 deletions(-) create mode 100644 Stdlib.Data.Result-src.html create mode 100644 Stdlib.Data.Result.Base-src.html create mode 100644 Stdlib.Data.Result.Base.html create mode 100644 Stdlib.Data.Result.html diff --git a/Juvix.Builtin.V1.Bool-src.html b/Juvix.Builtin.V1.Bool-src.html index e8408850..ec3a8c34 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Juvix.Builtin.V1.Bool.html b/Juvix.Builtin.V1.Bool.html index 8fcb7d8b..6d54ce72 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 +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 350d55e9..a08e3911 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Juvix.Builtin.V1.Fixity.html b/Juvix.Builtin.V1.Fixity.html index 3bb91071..b331eb62 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

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/.config/juvix/0.6.2/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.2/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.2/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.2/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.2/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.2/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.2/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.2/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.2/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.2/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.2/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.2/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.2/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.2/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.2/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

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 3d86a1bc..41e362cd 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Juvix.Builtin.V1.List.html b/Juvix.Builtin.V1.List.html index eadf2a80..9d804821 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 +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 3647f097..da79a957 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Juvix.Builtin.V1.Maybe.html b/Juvix.Builtin.V1.Maybe.html index 246042b1..56b1f904 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 +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 9c314529..7fdcc4ba 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 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 caa728d1..515742f5 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Juvix.Builtin.V1.Nat.Base.html b/Juvix.Builtin.V1.Nat.Base.html index be6f68f8..3374e3e4 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 57befb09..54ad0f0d 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

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 0414b0cc..e845eac1 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Juvix.Builtin.V1.String.html b/Juvix.Builtin.V1.String.html index 84c5bedd..6c85f469 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 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 175dabbd..f57bd827 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Juvix.Builtin.V1.Trait.Natural.html b/Juvix.Builtin.V1.Trait.Natural.html index 6da943c3..4439d80d 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 c9ccf3f7..b8ba234d 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Cairo.Poseidon.html b/Stdlib.Cairo.Poseidon.html index 1160745c..82c314ab 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 47219376..d2ed430d 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Data.Bool.Base-src.html b/Stdlib.Data.Bool.Base-src.html index 48e7244a..06b67846 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Data.Bool.Base.html b/Stdlib.Data.Bool.Base.html index d6f75de1..4f9e4420 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

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 6c36d075..977a3d4e 100644 --- a/Stdlib.Data.Bool.html +++ b/Stdlib.Data.Bool.html @@ -2,4 +2,4 @@ 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.Field-src.html b/Stdlib.Data.Field-src.html index 0c338486..f63ecbd2 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Data.Field.Base-src.html b/Stdlib.Data.Field.Base-src.html index 049e6b50..a67da4fe 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Data.Field.Base.html b/Stdlib.Data.Field.Base.html index eade9a49..7e9492fe 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 50ef1a27..7884bccd 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 826b0056..38216df5 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Data.Fixity.html b/Stdlib.Data.Fixity.html index 39c9b0bc..2365f652 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 3f05306e..a5015d67 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Data.Int.Base-src.html b/Stdlib.Data.Int.Base-src.html index 5f8bdcad..9b5c865d 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Data.Int.Base.html b/Stdlib.Data.Int.Base.html index 91c78b65..09502208 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 a1a80216..c7f92346 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Data.Int.Ord.html b/Stdlib.Data.Int.Ord.html index a8fcff82..0a3d300e 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

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 e1926894..be6ac9b6 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 0e08ad70..912b7822 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Data.List.Base-src.html b/Stdlib.Data.List.Base-src.html index 0aec38e9..be7a7668 100644 --- a/Stdlib.Data.List.Base-src.html +++ b/Stdlib.Data.List.Base-src.html @@ -13,209 +13,218 @@ --- 𝒪(𝓃). Returns ;true; if the given --- object is in the ;List;. {-# specialize: [1] #-} -elem {A} (eq : A → A → Bool) (s : A) : List A → Bool +elem {A} (eq : A → A → Bool) (s : A) : List A → Bool | nil := false - | (x :: xs) := eq s x || elem eq s xs; + | (x :: xs) := eq s x || elem eq s xs; + +--- 𝒪(𝓃). Returns the leftmost element of the list satisfying the predicate or +--- nothing if there's no such element. +find {A} (predicate : A → Bool) : List A → Maybe A + | nil := nothing + | (x :: xs) := + if + | predicate x := just x + | else := find predicate xs; --- Right-associative fold. {-# specialize: [1] #-} -foldr {A B} (f : A → B → B) (z : B) : List A → B - | nil := z - | (h :: hs) := f h (foldr f z hs); +foldr {A B} (f : A → B → B) (z : B) : List A → B + | nil := z + | (h :: hs) := f h (foldr f z hs); syntax iterator rfor {init := 1; range := 1}; {-# specialize: [1] #-} -rfor {A B} (f : B → A → B) (acc : B) : List A → B - | nil := acc - | (x :: xs) := f (rfor f acc xs) x; +rfor {A B} (f : B → A → B) (acc : B) : List A → B + | nil := acc + | (x :: xs) := f (rfor f acc xs) x; --- Left-associative and tail-recursive fold. {-# specialize: [1] #-} -foldl {A B} (f : B → A → B) (z : B) : List A → B - | nil := z - | (h :: hs) := foldl f (f z h) hs; +foldl {A B} (f : B → A → B) (z : B) : List A → B + | nil := z + | (h :: hs) := foldl f (f z h) hs; syntax iterator for {init := 1; range := 1}; {-# inline: 0 #-} -for : {A B : Type} → (B → A → B) → B → List A → B := foldl; +for : {A B : Type} → (B → A → B) → B → List A → B := foldl; syntax iterator map {init := 0; range := 1}; --- 𝒪(𝓃). Maps a function over each element of a ;List;. {-# specialize: [1] #-} -map {A B} (f : A → B) : List A → List B +map {A B} (f : A → B) : List A → List B | nil := nil - | (h :: hs) := f h :: map f hs; + | (h :: hs) := f h :: map f hs; syntax iterator filter {init := 0; range := 1}; --- 𝒪(𝓃). Filters a ;List; according to a given predicate, i.e., --- keeps the elements for which the given predicate returns ;true;. {-# specialize: [1] #-} -filter {A} (f : A → Bool) : List A → List A +filter {A} (f : A → Bool) : List A → List A | nil := nil - | (h :: hs) := ite (f h) (h :: filter f hs) (filter f hs); + | (h :: hs) := ite (f h) (h :: filter f hs) (filter f hs); --- 𝒪(𝓃). Returns the length of the ;List;. -length {A} (l : List A) : Nat := for (acc := zero) (_ in l) {suc acc}; +length {A} (l : List A) : Nat := for (acc := zero) (_ in l) {suc acc}; --- 𝒪(𝓃). Returns the given ;List; in reverse order. -reverse {A} (l : List A) : List A := for (acc := nil) (x in l) {x :: acc}; +reverse {A} (l : List A) : List A := for (acc := nil) (x in l) {x :: acc}; --- Returns a ;List; of length n where every element is the given value. -replicate {A} : Nat → A → List A +replicate {A} : Nat → A → List A | zero _ := nil - | (suc n) x := x :: replicate n x; + | (suc n) x := x :: replicate n x; --- Takes the first n elements of a ;List;. -take {A} : Nat → List A → List A - | (suc n) (x :: xs) := x :: take n xs +take {A} : Nat → List A → List A + | (suc n) (x :: xs) := x :: take n xs | _ _ := nil; --- Drops the first n elements of a ;List;. -drop {A} : Nat → List A → List A - | (suc n) (x :: xs) := drop n xs - | _ xs := xs; +drop {A} : Nat → List A → List A + | (suc n) (x :: xs) := drop n xs + | _ xs := xs; --- 𝒪(𝓃). splitAt n xs returns a tuple where first element is xs --- prefix of length n and second element is the remainder of the ;List;. -splitAt {A} : Nat → List A → Pair (List A) (List A) +splitAt {A} : Nat → List A → Pair (List A) (List A) | _ nil := nil, nil - | zero xs := nil, xs - | (suc zero) (x :: xs) := x :: nil, xs - | (suc m) (x :: xs) := case splitAt m xs of l1, l2 := x :: l1, l2; + | zero xs := nil, xs + | (suc zero) (x :: xs) := x :: nil, xs + | (suc m) (x :: xs) := case splitAt m xs of l1, l2 := x :: l1, l2; --- 𝒪(𝓃 + 𝓂). Merges two lists according the given ordering. terminating -merge {A} {{Ord A}} : List A → List A → List A - | xs@(x :: xs') ys@(y :: ys') := +merge {A} {{Ord A}} : List A → List A → List A + | xs@(x :: xs') ys@(y :: ys') := if - | isLT (Ord.cmp x y) := x :: merge xs' ys - | else := y :: merge xs ys' - | nil ys := ys - | xs nil := xs; + | isLT (Ord.cmp x y) := x :: merge xs' ys + | else := y :: merge xs ys' + | nil ys := ys + | xs nil := xs; --- 𝒪(𝓃). Returns a tuple where the first component has the items that --- satisfy the predicate and the second component has the elements that don't. -partition {A} (f : A → Bool) : List A → Pair (List A) (List A) +partition {A} (f : A → Bool) : List A → Pair (List A) (List A) | nil := nil, nil - | (x :: xs) := - case partition f xs of l1, l2 := ite (f x) (x :: l1, l2) (l1, x :: l2); + | (x :: xs) := + case partition f xs of l1, l2 := ite (f x) (x :: l1, l2) (l1, x :: l2); syntax operator ++ cons; --- Concatenates two ;List;s. -++ : {A : Type} → List A → List A → List A - | nil ys := ys - | (x :: xs) ys := x :: xs ++ ys; +++ : {A : Type} → List A → List A → List A + | nil ys := ys + | (x :: xs) ys := x :: xs ++ ys; --- 𝒪(𝓃). Append an element. -snoc {A} (xs : List A) (x : A) : List A := xs ++ x :: nil; +snoc {A} (xs : List A) (x : A) : List A := xs ++ x :: nil; --- Concatenates a ;List; of ;List;s. -flatten : {A : Type} → List (List A) → List A := foldl (++) nil; +flatten : {A : Type} → List (List A) → List A := foldl (++) nil; --- 𝒪(𝓃). Inserts the given element before every element in the given ;List;. -prependToAll {A} (sep : A) : List A → List A +prependToAll {A} (sep : A) : List A → List A | nil := nil - | (x :: xs) := sep :: x :: prependToAll sep xs; + | (x :: xs) := sep :: x :: prependToAll sep xs; --- 𝒪(𝓃). Inserts the given element inbetween every two elements in the given ;List;. -intersperse {A} (sep : A) : List A → List A +intersperse {A} (sep : A) : List A → List A | nil := nil - | (x :: xs) := x :: prependToAll sep xs; + | (x :: xs) := x :: prependToAll sep xs; --- 𝒪(1). Drops the first element of a ;List;. -tail {A} : List A → List A - | (_ :: xs) := xs +tail {A} : List A → List A + | (_ :: xs) := xs | nil := nil; - -head {A} (a : A) : List A -> A - | (x :: _) := x - | nil := a; + +head {A} (a : A) : List A -> A + | (x :: _) := x + | nil := a; syntax iterator any {init := 0; range := 1}; --- 𝒪(𝓃). Returns ;true; if at least one element of the ;List; satisfies the predicate. {-# specialize: [1] #-} -any {A} (f : A → Bool) : List A → Bool +any {A} (f : A → Bool) : List A → Bool | nil := false - | (x :: xs) := ite (f x) true (any f xs); + | (x :: xs) := ite (f x) true (any f xs); syntax iterator all {init := 0; range := 1}; --- 𝒪(𝓃). Returns ;true; if all elements of the ;List; satisfy the predicate. {-# specialize: [1] #-} -all {A} (f : A -> Bool) : List A -> Bool +all {A} (f : A -> Bool) : List A -> Bool | nil := true - | (x :: xs) := ite (f x) (all f xs) false; + | (x :: xs) := ite (f x) (all f xs) false; --- 𝒪(1). Returns ;true; if the ;List; is empty. -null {A} : List A → Bool +null {A} : List A → Bool | nil := true | _ := false; --- 𝒪(min(𝓂, 𝓃)). Returns a list containing the results of applying a function --- to each pair of elements from the input lists. {-# specialize: [1] #-} -zipWith {A B C} (f : A -> B -> C) : List A -> List B -> List C +zipWith {A B C} (f : A -> B -> C) : List A -> List B -> List C | nil _ := nil | _ nil := nil - | (x :: xs) (y :: ys) := f x y :: zipWith f xs ys; + | (x :: xs) (y :: ys) := f x y :: zipWith f xs ys; --- 𝒪(min(𝓂, 𝓃)). Returns a list of pairs formed from the input lists. -zip {A B} : List A -> List B -> List (Pair A B) +zip {A B} : List A -> List B -> List (Pair A B) | nil _ := nil | _ nil := nil - | (x :: xs) (y :: ys) := (x, y) :: zip xs ys; + | (x :: xs) (y :: ys) := (x, y) :: zip xs ys; --- 𝒪(𝓃 log 𝓃). Sorts a list of elements in ascending order using the MergeSort --- algorithm. -mergeSort {A} {{Ord A}} (l : List A) : List A := +mergeSort {A} {{Ord A}} (l : List A) : List A := let terminating - go : Nat -> List A -> List A + go : Nat -> List A -> List A | zero _ := nil - | (suc zero) xs := xs - | len xs := + | (suc zero) xs := xs + | len xs := let - len' : Nat := div len (suc (suc zero)); - splitXs : Pair (List A) (List A) := splitAt len' xs; - left : List A := fst splitXs; - right : List A := snd splitXs; - in merge (go len' left) (go (sub len len') right); - in go (length l) l; + len' : Nat := div len (suc (suc zero)); + splitXs : Pair (List A) (List A) := splitAt len' xs; + left : List A := fst splitXs; + right : List A := snd splitXs; + in merge (go len' left) (go (sub len len') right); + in go (length l) l; --- On average 𝒪(𝓃 log 𝓃), worst case 𝒪(𝓃²). Sorts a list of elements in --- ascending order using the QuickSort algorithm. terminating -quickSort {A} {{Ord A}} : List A → List A := +quickSort {A} {{Ord A}} : List A → List A := let terminating - go : List A → List A + go : List A → List A | nil := nil - | xs@(_ :: nil) := xs - | (x :: xs) := - case partition (Ord.cmp x >> isGT) xs of l1, l2 := go l1 ++ x :: go l2; - in go; + | xs@(_ :: nil) := xs + | (x :: xs) := + case partition (Ord.cmp x >> isGT) xs of l1, l2 := go l1 ++ x :: go l2; + in go; --- 𝒪(𝓃) Filters out every ;nothing; from a ;List;. -catMaybes {A} : List (Maybe A) -> List A +catMaybes {A} : List (Maybe A) -> List A | nil := nil - | (just h :: hs) := h :: catMaybes hs - | (nothing :: hs) := catMaybes hs; + | (just h :: hs) := h :: catMaybes hs + | (nothing :: hs) := catMaybes hs; syntax iterator concatMap {init := 0; range := 1}; --- Applies a function to every item on a ;List; and concatenates the result. --- 𝒪(𝓃), where 𝓃 is the number of items in the resulting list. -concatMap {A B} (f : A -> List B) : List A -> List B := map f >> flatten; +concatMap {A B} (f : A -> List B) : List A -> List B := map f >> flatten; --- 𝒪(𝓃 * 𝓂). Transposes a ;List; of ;List;s interpreted as a matrix. -transpose {A} : List (List A) -> List (List A) +transpose {A} : List (List A) -> List (List A) | nil := nil - | (xs :: nil) := map λ {x := x :: nil} xs - | (xs :: xss) := zipWith (::) xs (transpose xss); -Last modified on 2024-07-01 3:19 UTC \ No newline at end of file + | (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 diff --git a/Stdlib.Data.List.Base.html b/Stdlib.Data.List.Base.html index 9f7740f4..a4daca5b 100644 --- a/Stdlib.Data.List.Base.html +++ b/Stdlib.Data.List.Base.html @@ -1,4 +1,4 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.List.Base

Definitions

import Juvix.Builtin.V1.List open public

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

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

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 +Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.List.Base

Definitions

import Juvix.Builtin.V1.List open public

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

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

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

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

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

Right-associative fold.

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

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

Left-associative and tail-recursive fold.

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

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 diff --git a/Stdlib.Data.List.html b/Stdlib.Data.List.html index c519f481..2fc88b85 100644 --- a/Stdlib.Data.List.html +++ b/Stdlib.Data.List.html @@ -2,4 +2,4 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.List

Definitions

import Stdlib.Data.List.Base open public

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

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

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

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

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

\ 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 1f628d1e..13b047b2 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Data.Maybe.Base-src.html b/Stdlib.Data.Maybe.Base-src.html index 675b9658..d7fbadd7 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Data.Maybe.Base.html b/Stdlib.Data.Maybe.Base.html index b75efd6c..f84dc747 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} (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

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 803b6353..51ceace2 100644 --- a/Stdlib.Data.Maybe.html +++ b/Stdlib.Data.Maybe.html @@ -2,4 +2,4 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Maybe

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 596fea6a..aa3bb329 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Data.Nat.Base-src.html b/Stdlib.Data.Nat.Base-src.html index bd3f76e1..7407628c 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Data.Nat.Base.html b/Stdlib.Data.Nat.Base.html index 607f2deb..87eda56c 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 2b8fd568..cb455fe2 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Data.Nat.Ord.html b/Stdlib.Data.Nat.Ord.html index ad97f99d..f056fd18 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

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 7ee36d05..f420ea19 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 d9fee50a..0844380c 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Data.Pair.Base-src.html b/Stdlib.Data.Pair.Base-src.html index c5b65e6a..cd44f561 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Data.Pair.Base.html b/Stdlib.Data.Pair.Base.html index 486ec097..99e8550f 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

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

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 69c8f45e..fd932801 100644 --- a/Stdlib.Data.Pair.html +++ b/Stdlib.Data.Pair.html @@ -2,4 +2,4 @@ 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.Result-src.html b/Stdlib.Data.Result-src.html new file mode 100644 index 00000000..fd8bb7f7 --- /dev/null +++ b/Stdlib.Data.Result-src.html @@ -0,0 +1,28 @@ + +
module Stdlib.Data.Result;
+
+import Stdlib.Data.Result.Base open public;
+import Stdlib.Data.Bool.Base open;
+
+import Stdlib.Trait.Eq open;
+import Stdlib.Trait.Ord open;
+
+instance
+ordResultI {A B} {{Ord A}} {{Ord B}} : Ord (Result A B) :=
+  mkOrd@{
+    cmp : Result A B -> Result A B -> Ordering
+      | (error a1) (error a2) := Ord.cmp a1 a2
+      | (ok b1) (ok b2) := Ord.cmp b1 b2
+      | (error _) (ok _) := LT
+      | (ok _) (error _) := GT
+  };
+
+instance
+eqResultI {A B} {{Eq A}} {{Eq B}} : Eq (Result A B) :=
+  mkEq@{
+    eq : Result A B -> Result A B -> Bool
+      | (error a1) (error a2) := a1 == a2
+      | (ok b1) (ok b2) := b1 == b2
+      | _ _ := false
+  };
+
Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Data.Result.Base-src.html b/Stdlib.Data.Result.Base-src.html new file mode 100644 index 00000000..0f0eaf8e --- /dev/null +++ b/Stdlib.Data.Result.Base-src.html @@ -0,0 +1,56 @@ + +
module Stdlib.Data.Result.Base;
+
+import Stdlib.Data.Bool.Base open;
+import Stdlib.Data.Maybe.Base open;
+import Stdlib.Function open;
+
+--- The Result type represents either a success with a value of `ok` or an error
+--- with value `error`.
+type Result E A :=
+  | error E
+  | ok A;
+
+--- Apply the onError function if the value is ;error; or apply the
+--- onOk function if the value is ;ok;.
+handleResult {E A B} (onError : E -> B) (onOk : A -> B) : Result E A -> B
+  | (error a) := onError a
+  | (ok a) := onOk a;
+
+--- Apply a function to the ;error; value of a Result.
+mapError {A E1 E2} (f : E1 -> E2) : Result E1 A -> Result E2 A :=
+  handleResult (f >> error) ok;
+
+--- Apply a function to the ;ok; value of a Result.
+mapOk {E A C} (f : A -> C) : Result E A -> Result E C :=
+  handleResult error (f >> ok);
+
+--- Return ;true; if the value is an ;error;, otherwise ;false;.
+isError {E A} : Result E A -> Bool
+  | (error _) := true
+  | (ok _) := false;
+
+--- Return ;true; if the value is ;ok;, otherwise ;false;.
+isOk {E A} : Result E A -> Bool
+  | (error _) := false
+  | (ok _) := true;
+
+--- Return the contents of an ;error; value, otherwise return a default.
+fromError {E A} (default : E) : Result E A -> E
+  | (error a) := a
+  | (ok _) := default;
+
+--- Return the contents of an ;ok; value, otherwise return a default.
+fromOk {E A} (default : A) : Result E A -> A
+  | (error _) := default
+  | (ok b) := b;
+
+--- Convert a Result to a Maybe. An ;error; value becomes `nothing`.
+resultToMaybe {E A} : Result E A -> Maybe A :=
+  handleResult (const nothing) just;
+
+--- Convert a Maybe to a Result. A ;nothing; value becomes `error defaultError`.
+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 diff --git a/Stdlib.Data.Result.Base.html b/Stdlib.Data.Result.Base.html new file mode 100644 index 00000000..f38e62bf --- /dev/null +++ b/Stdlib.Data.Result.Base.html @@ -0,0 +1,2 @@ + +Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Result.Base

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 new file mode 100644 index 00000000..688c5872 --- /dev/null +++ b/Stdlib.Data.Result.html @@ -0,0 +1,4 @@ + +Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Result

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 diff --git a/Stdlib.Data.String-src.html b/Stdlib.Data.String-src.html index fa16d17a..e4f83b7b 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Data.String.Base-src.html b/Stdlib.Data.String.Base-src.html index 6b4b75b8..8cfd5d03 100644 --- a/Stdlib.Data.String.Base-src.html +++ b/Stdlib.Data.String.Base-src.html @@ -7,8 +7,8 @@ import Stdlib.Data.Fixity open; --- Concatenates a ;List; of ;String;s. -concatStr : List String -> String := foldl (++str) ""; +concatStr : List String -> String := foldl (++str) ""; --- Joins a ;List; of ;String;s with "\n". -unlines : List String -> String := intersperse "\n" >> concatStr; -Last modified on 2024-07-01 3:19 UTC \ No newline at end of file +unlines : List String -> String := intersperse "\n" >> concatStr; +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Data.String.Base.html b/Stdlib.Data.String.Base.html index f127100c..3a2d8469 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 : 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

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 2abff68b..53a157da 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Data.String.Ord.html b/Stdlib.Data.String.Ord.html index f7735dda..099f7c83 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 +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 f11c6860..f3a29dce 100644 --- a/Stdlib.Data.String.html +++ b/Stdlib.Data.String.html @@ -1,4 +1,4 @@ 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.Unit-src.html b/Stdlib.Data.Unit-src.html index 8b3d5023..72b4f08e 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Data.Unit.html b/Stdlib.Data.Unit.html index 1e9d16d8..c22f2217 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 c40d2d97..3f9542f1 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Debug.Fail.html b/Stdlib.Debug.Fail.html index 4fcdc887..1e5a2892 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} → 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 955852e6..ab23aa5d 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Function.html b/Stdlib.Function.html index 657b3d5b..3b229af5 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 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 c2a333c6..66259568 100644 --- a/Stdlib.Prelude-src.html +++ b/Stdlib.Prelude-src.html @@ -13,8 +13,9 @@ 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; -Last modified on 2024-07-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Prelude.html b/Stdlib.Prelude.html index 7a9e22c1..8e73014c 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.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 4850c0db..e5e6ca39 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.System.IO.Base-src.html b/Stdlib.System.IO.Base-src.html index a9389262..6b9958c8 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.System.IO.Base.html b/Stdlib.System.IO.Base.html index f23c0538..c5360f86 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 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 0c102486..deb3f36b 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.System.IO.Bool.html b/Stdlib.System.IO.Bool.html index 3209d1b4..f123284d 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 +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 b7b2e82b..87dad019 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.System.IO.Int.html b/Stdlib.System.IO.Int.html index 3e4424cd..9a065f52 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 +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 e49c95ea..c9983483 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.System.IO.Nat.html b/Stdlib.System.IO.Nat.html index 36b0bbd5..8fc55ac9 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 +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 23b0bfb4..0e687f8d 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.System.IO.String.html b/Stdlib.System.IO.String.html index 090063ee..259cc378 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 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 cc8b6aa2..48a64745 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 9f839e96..c0003714 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Trait.DivMod-src.html b/Stdlib.Trait.DivMod-src.html index 42ec26d2..d1133e95 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Trait.DivMod.html b/Stdlib.Trait.DivMod.html index fd21f050..f217a525 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 17463c18..43348121 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Eq.html b/Stdlib.Trait.Eq.html index 3be925bd..30a3395d 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#

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 c0aafa5b..82daf715 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Integral.html b/Stdlib.Trait.Integral.html index 675b84c2..0741313b 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 e948074f..b7f73a20 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Natural.html b/Stdlib.Trait.Natural.html index 0f2486fe..08942aed 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 69fe8214..1e2faf25 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Numeric.html b/Stdlib.Trait.Numeric.html index 9850b3e4..646a5a8f 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 19822728..2ffa8294 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Ord.html b/Stdlib.Trait.Ord.html index 520fffb1..9bd3ddbd 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

| 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 90025a53..eee3f057 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Partial.html b/Stdlib.Trait.Partial.html index 17dc5ba0..65916ebd 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 +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 8aedcc71..eb99fa1f 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Show.html b/Stdlib.Trait.Show.html index ce3a3793..e064fe33 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 +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 a99ab67b..870877e7 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.Partial open public

import Stdlib.Trait.Natural open public

import Stdlib.Trait.Integral open public

import Stdlib.Trait.Numeric open public

import Stdlib.Trait.DivMod open public

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

Stdlib.Trait

Definitions

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

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

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

import Stdlib.Trait.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 d619a0fa..05918f39 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-01 3:19 UTC \ No newline at end of file +Last modified on 2024-07-10 15:52 UTC \ No newline at end of file diff --git a/index.html b/index.html index 6155eab1..b37ffcd6 100644 --- a/index.html +++ b/index.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1
\ No newline at end of file +Juvix Documentation
stdlib - 0.0.1
\ No newline at end of file