diff --git a/Stdlib.Data.Bool-src.html b/Stdlib.Data.Bool-src.html index 74086f4e..ccedf8dd 100644 --- a/Stdlib.Data.Bool-src.html +++ b/Stdlib.Data.Bool-src.html @@ -32,4 +32,4 @@ | true := "true" | false := "false" }; -Last modified on 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Data.Bool.Base-src.html b/Stdlib.Data.Bool.Base-src.html index 5549865a..d57d7b40 100644 --- a/Stdlib.Data.Bool.Base-src.html +++ b/Stdlib.Data.Bool.Base-src.html @@ -41,4 +41,4 @@ --- Logical conjunction. and (a b : Bool) : Bool := a && b; -Last modified on 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Data.Bool.Base.html b/Stdlib.Data.Bool.Base.html index dcba43cb..90a36d5a 100644 --- a/Stdlib.Data.Bool.Base.html +++ b/Stdlib.Data.Bool.Base.html @@ -3,4 +3,4 @@ type BoolSource#

Inductive definition of booleans.

Constructors

| true
| false

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 -if : {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 +if : {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 645c16a4..b75e66ed 100644 --- a/Stdlib.Data.Bool.html +++ b/Stdlib.Data.Bool.html @@ -2,4 +2,4 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Bool

Description

Definitions

import Stdlib.Data.Bool.Base open public

instance boolEqI : Eq BoolSource#

instance boolOrdI : Ord BoolSource#

instance -showBoolI : Show BoolSource#

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

\ No newline at end of file diff --git a/Stdlib.Data.Fixity-src.html b/Stdlib.Data.Fixity-src.html index 03105a9d..1384eaa9 100644 --- a/Stdlib.Data.Fixity-src.html +++ b/Stdlib.Data.Fixity-src.html @@ -22,4 +22,4 @@ syntax fixity multiplicative := binary {assoc := left; above := [additive]}; syntax fixity composition := binary {assoc := right; above := [multiplicative]}; -Last modified on 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Data.Fixity.html b/Stdlib.Data.Fixity.html index 1902aa9f..c2a47232 100644 --- a/Stdlib.Data.Fixity.html +++ b/Stdlib.Data.Fixity.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Fixity

Description

Definitions

syntax fixity noneSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/work/juvix-stdlib/juvix-stdlib/Stdlib/Data/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 3}, _locCol = Pos {_unPos = 23}, _locOffset = Pos {_unPos = 50}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 3}, _locCol = Pos {_unPos = 27}, _locOffset = Pos {_unPos = 54}}}, _withLocParam = None}

syntax fixity rappSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/work/juvix-stdlib/juvix-stdlib/Stdlib/Data/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 5}, _locCol = Pos {_unPos = 23}, _locOffset = Pos {_unPos = 79}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 5}, _locCol = Pos {_unPos = 30}, _locOffset = Pos {_unPos = 86}}}, _withLocParam = Binary}, right-associative

syntax fixity lappSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/work/juvix-stdlib/juvix-stdlib/Stdlib/Data/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 6}, _locCol = Pos {_unPos = 23}, _locOffset = Pos {_unPos = 126}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 6}, _locCol = Pos {_unPos = 30}, _locOffset = Pos {_unPos = 133}}}, _withLocParam = Binary}, left-associative
Same precedence as rapp

syntax fixity seqSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/work/juvix-stdlib/juvix-stdlib/Stdlib/Data/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 7}, _locCol = Pos {_unPos = 22}, _locOffset = Pos {_unPos = 185}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 7}, _locCol = Pos {_unPos = 29}, _locOffset = Pos {_unPos = 192}}}, _withLocParam = Binary}, left-associative
Higher precedence than: lapp,

syntax fixity functorSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/work/juvix-stdlib/juvix-stdlib/Stdlib/Data/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 9}, _locCol = Pos {_unPos = 26}, _locOffset = Pos {_unPos = 252}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 9}, _locCol = Pos {_unPos = 33}, _locOffset = Pos {_unPos = 259}}}, _withLocParam = Binary}, right-associative

syntax fixity logicalSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/work/juvix-stdlib/juvix-stdlib/Stdlib/Data/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 11}, _locCol = Pos {_unPos = 26}, _locOffset = Pos {_unPos = 303}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 11}, _locCol = Pos {_unPos = 33}, _locOffset = Pos {_unPos = 310}}}, _withLocParam = Binary}, right-associative
Higher precedence than: seq,

syntax fixity comparisonSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/work/juvix-stdlib/juvix-stdlib/Stdlib/Data/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 12}, _locCol = Pos {_unPos = 29}, _locOffset = Pos {_unPos = 372}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 12}, _locCol = Pos {_unPos = 36}, _locOffset = Pos {_unPos = 379}}}, _withLocParam = Binary}
Higher precedence than: logical,

syntax fixity pairSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/work/juvix-stdlib/juvix-stdlib/Stdlib/Data/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 14}, _locCol = Pos {_unPos = 23}, _locOffset = Pos {_unPos = 439}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 14}, _locCol = Pos {_unPos = 30}, _locOffset = Pos {_unPos = 446}}}, _withLocParam = Binary}, right-associative

syntax fixity consSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/work/juvix-stdlib/juvix-stdlib/Stdlib/Data/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 15}, _locCol = Pos {_unPos = 23}, _locOffset = Pos {_unPos = 486}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 15}, _locCol = Pos {_unPos = 30}, _locOffset = Pos {_unPos = 493}}}, _withLocParam = Binary}, right-associative
Higher precedence than: pair,

syntax fixity stepSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/work/juvix-stdlib/juvix-stdlib/Stdlib/Data/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 17}, _locCol = Pos {_unPos = 23}, _locOffset = Pos {_unPos = 551}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 17}, _locCol = Pos {_unPos = 30}, _locOffset = Pos {_unPos = 558}}}, _withLocParam = Binary}, right-associative

syntax fixity rangeSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/work/juvix-stdlib/juvix-stdlib/Stdlib/Data/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 18}, _locCol = Pos {_unPos = 24}, _locOffset = Pos {_unPos = 599}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 18}, _locCol = Pos {_unPos = 31}, _locOffset = Pos {_unPos = 606}}}, _withLocParam = Binary}, right-associative
Higher precedence than: step,

syntax fixity additiveSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/work/juvix-stdlib/juvix-stdlib/Stdlib/Data/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 20}, _locCol = Pos {_unPos = 27}, _locOffset = Pos {_unPos = 668}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 20}, _locCol = Pos {_unPos = 34}, _locOffset = Pos {_unPos = 675}}}, _withLocParam = Binary}, left-associative
Higher precedence than: comparison, range, cons,

syntax fixity multiplicativeSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/work/juvix-stdlib/juvix-stdlib/Stdlib/Data/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 21}, _locCol = Pos {_unPos = 33}, _locOffset = Pos {_unPos = 760}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 21}, _locCol = Pos {_unPos = 40}, _locOffset = Pos {_unPos = 767}}}, _withLocParam = Binary}, left-associative
Higher precedence than: additive,

syntax fixity compositionSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/work/juvix-stdlib/juvix-stdlib/Stdlib/Data/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 23}, _locCol = Pos {_unPos = 30}, _locOffset = Pos {_unPos = 835}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 23}, _locCol = Pos {_unPos = 37}, _locOffset = Pos {_unPos = 842}}}, _withLocParam = Binary}, right-associative
Higher precedence than: multiplicative,
\ No newline at end of file +Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Fixity

Description

Definitions

syntax fixity noneSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/work/juvix-stdlib/juvix-stdlib/Stdlib/Data/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 3}, _locCol = Pos {_unPos = 23}, _locOffset = Pos {_unPos = 50}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 3}, _locCol = Pos {_unPos = 27}, _locOffset = Pos {_unPos = 54}}}, _withLocParam = None}

syntax fixity rappSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/work/juvix-stdlib/juvix-stdlib/Stdlib/Data/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 5}, _locCol = Pos {_unPos = 23}, _locOffset = Pos {_unPos = 79}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 5}, _locCol = Pos {_unPos = 30}, _locOffset = Pos {_unPos = 86}}}, _withLocParam = Binary}, right-associative

syntax fixity lappSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/work/juvix-stdlib/juvix-stdlib/Stdlib/Data/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 6}, _locCol = Pos {_unPos = 23}, _locOffset = Pos {_unPos = 126}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 6}, _locCol = Pos {_unPos = 30}, _locOffset = Pos {_unPos = 133}}}, _withLocParam = Binary}, left-associative
Same precedence as rapp

syntax fixity seqSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/work/juvix-stdlib/juvix-stdlib/Stdlib/Data/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 7}, _locCol = Pos {_unPos = 22}, _locOffset = Pos {_unPos = 185}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 7}, _locCol = Pos {_unPos = 29}, _locOffset = Pos {_unPos = 192}}}, _withLocParam = Binary}, left-associative
Higher precedence than: lapp,

syntax fixity functorSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/work/juvix-stdlib/juvix-stdlib/Stdlib/Data/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 9}, _locCol = Pos {_unPos = 26}, _locOffset = Pos {_unPos = 252}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 9}, _locCol = Pos {_unPos = 33}, _locOffset = Pos {_unPos = 259}}}, _withLocParam = Binary}, right-associative

syntax fixity logicalSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/work/juvix-stdlib/juvix-stdlib/Stdlib/Data/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 11}, _locCol = Pos {_unPos = 26}, _locOffset = Pos {_unPos = 303}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 11}, _locCol = Pos {_unPos = 33}, _locOffset = Pos {_unPos = 310}}}, _withLocParam = Binary}, right-associative
Higher precedence than: seq,

syntax fixity comparisonSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/work/juvix-stdlib/juvix-stdlib/Stdlib/Data/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 12}, _locCol = Pos {_unPos = 29}, _locOffset = Pos {_unPos = 372}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 12}, _locCol = Pos {_unPos = 36}, _locOffset = Pos {_unPos = 379}}}, _withLocParam = Binary}
Higher precedence than: logical,

syntax fixity pairSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/work/juvix-stdlib/juvix-stdlib/Stdlib/Data/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 14}, _locCol = Pos {_unPos = 23}, _locOffset = Pos {_unPos = 439}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 14}, _locCol = Pos {_unPos = 30}, _locOffset = Pos {_unPos = 446}}}, _withLocParam = Binary}, right-associative

syntax fixity consSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/work/juvix-stdlib/juvix-stdlib/Stdlib/Data/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 15}, _locCol = Pos {_unPos = 23}, _locOffset = Pos {_unPos = 486}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 15}, _locCol = Pos {_unPos = 30}, _locOffset = Pos {_unPos = 493}}}, _withLocParam = Binary}, right-associative
Higher precedence than: pair,

syntax fixity stepSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/work/juvix-stdlib/juvix-stdlib/Stdlib/Data/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 17}, _locCol = Pos {_unPos = 23}, _locOffset = Pos {_unPos = 551}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 17}, _locCol = Pos {_unPos = 30}, _locOffset = Pos {_unPos = 558}}}, _withLocParam = Binary}, right-associative

syntax fixity rangeSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/work/juvix-stdlib/juvix-stdlib/Stdlib/Data/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 18}, _locCol = Pos {_unPos = 24}, _locOffset = Pos {_unPos = 599}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 18}, _locCol = Pos {_unPos = 31}, _locOffset = Pos {_unPos = 606}}}, _withLocParam = Binary}, right-associative
Higher precedence than: step,

syntax fixity additiveSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/work/juvix-stdlib/juvix-stdlib/Stdlib/Data/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 20}, _locCol = Pos {_unPos = 27}, _locOffset = Pos {_unPos = 668}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 20}, _locCol = Pos {_unPos = 34}, _locOffset = Pos {_unPos = 675}}}, _withLocParam = Binary}, left-associative
Higher precedence than: comparison, range, cons,

syntax fixity multiplicativeSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/work/juvix-stdlib/juvix-stdlib/Stdlib/Data/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 21}, _locCol = Pos {_unPos = 33}, _locOffset = Pos {_unPos = 760}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 21}, _locCol = Pos {_unPos = 40}, _locOffset = Pos {_unPos = 767}}}, _withLocParam = Binary}, left-associative
Higher precedence than: additive,

syntax fixity compositionSource#

Fixity details

WithLoc {_withLocInt = Interval {_intervalFile = "/home/runner/work/juvix-stdlib/juvix-stdlib/Stdlib/Data/Fixity.juvix", _intervalStart = FileLoc {_locLine = Pos {_unPos = 23}, _locCol = Pos {_unPos = 30}, _locOffset = Pos {_unPos = 835}}, _intervalEnd = FileLoc {_locLine = Pos {_unPos = 23}, _locCol = Pos {_unPos = 37}, _locOffset = Pos {_unPos = 842}}}, _withLocParam = Binary}, right-associative
Higher precedence than: multiplicative,
\ No newline at end of file diff --git a/Stdlib.Data.Int-src.html b/Stdlib.Data.Int-src.html index a7cac8a3..d59c8573 100644 --- a/Stdlib.Data.Int-src.html +++ b/Stdlib.Data.Int-src.html @@ -51,4 +51,4 @@ - := (Int.-); fromInt (x : Int) : Int := x }; -Last modified on 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Data.Int.Base-src.html b/Stdlib.Data.Int.Base-src.html index 124cff6b..ea69611e 100644 --- a/Stdlib.Data.Int.Base-src.html +++ b/Stdlib.Data.Int.Base-src.html @@ -93,4 +93,4 @@ abs : Int -> Nat | (ofNat n) := n | (negSuc n) := suc n; -Last modified on 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Data.Int.Base.html b/Stdlib.Data.Int.Base.html index 0d4dc0bc..8ba0846f 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 01240aff..6e4f63d2 100644 --- a/Stdlib.Data.Int.Ord-src.html +++ b/Stdlib.Data.Int.Ord-src.html @@ -55,4 +55,4 @@ --- Returns the biggest ;Int;. max (x y : Int) : Int := if (x > y) x y; -Last modified on 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Data.Int.Ord.html b/Stdlib.Data.Int.Ord.html index 9850bc00..db1de9ff 100644 --- a/Stdlib.Data.Int.Ord.html +++ b/Stdlib.Data.Int.Ord.html @@ -2,4 +2,4 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Int.Ord

Description

Definitions

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

Tests for equality.

/= (m n : Int) : BoolSource#

Tests for inequality.

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

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

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

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

> (m n : Int) : BoolSource#

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

>= (m n : Int) : BoolSource#

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

compare (m n : Int) : OrderingSource#

Tests for Ordering.

min (x y : Int) : IntSource#

Returns the smallest Int.

max (x y : Int) : IntSource#

Returns the biggest Int.

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

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

> (m n : Int) : BoolSource#

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

>= (m n : Int) : BoolSource#

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

compare (m n : Int) : OrderingSource#

Tests for Ordering.

min (x y : Int) : IntSource#

Returns the smallest Int.

max (x y : Int) : IntSource#

Returns the biggest Int.

\ No newline at end of file diff --git a/Stdlib.Data.Int.html b/Stdlib.Data.Int.html index 2eec68ed..4a0d991d 100644 --- a/Stdlib.Data.Int.html +++ b/Stdlib.Data.Int.html @@ -5,4 +5,4 @@ ordIntI : Ord IntSource#

instance showIntI : Show IntSource#

instance naturalIntI : Natural IntSource#

instance -integralIntI : Integral IntSource#

\ No newline at end of file +integralIntI : Integral IntSource#

\ No newline at end of file diff --git a/Stdlib.Data.List-src.html b/Stdlib.Data.List-src.html index c5cfd8e1..f80cc296 100644 --- a/Stdlib.Data.List-src.html +++ b/Stdlib.Data.List-src.html @@ -51,4 +51,4 @@ | nil := "nil" | s := "(" ++str go s ++str ")" }; -Last modified on 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Data.List.Base-src.html b/Stdlib.Data.List.Base-src.html index f7e6817a..d008ebb3 100644 --- a/Stdlib.Data.List.Base-src.html +++ b/Stdlib.Data.List.Base-src.html @@ -225,4 +225,4 @@ | nil := nil | (xs :: nil) := map λ {x := x :: nil} xs | (xs :: xss) := zipWith (::) xs (transpose xss); -Last modified on 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Data.List.Base.html b/Stdlib.Data.List.Base.html index d938a9c0..ad6d6447 100644 --- a/Stdlib.Data.List.Base.html +++ b/Stdlib.Data.List.Base.html @@ -2,4 +2,4 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.List.Base

Description

Definitions

builtin list type List (a : Type)Source#

Inductive list.

Constructors

| nil

The empty list

| :: a (List a)

An element followed by a list

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 → List A × List ASource#

𝒪(𝓃). 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 → List A × List ASource#

𝒪(𝓃). 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 (A × B)Source#

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Stdlib.Data.List

Description

Definitions

import Stdlib.Data.List.Base open public

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

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

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

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

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

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

\ No newline at end of file diff --git a/Stdlib.Data.Maybe-src.html b/Stdlib.Data.Maybe-src.html index aad911c2..e97fdd8f 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 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Data.Maybe.Base-src.html b/Stdlib.Data.Maybe.Base-src.html index ccb2a396..57b57ad1 100644 --- a/Stdlib.Data.Maybe.Base-src.html +++ b/Stdlib.Data.Maybe.Base-src.html @@ -19,4 +19,4 @@ maybe {A B} (b : B) (f : A → B) : Maybe A → B | nothing := b | (just a) := f a; -Last modified on 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Data.Maybe.Base.html b/Stdlib.Data.Maybe.Base.html index d9d93778..7b176b62 100644 --- a/Stdlib.Data.Maybe.Base.html +++ b/Stdlib.Data.Maybe.Base.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Maybe.Base

Description

Definitions

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

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

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

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

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

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

Stdlib.Data.Maybe.Base

Description

Definitions

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

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 7bf7cdda..5a77707a 100644 --- a/Stdlib.Data.Maybe.html +++ b/Stdlib.Data.Maybe.html @@ -2,4 +2,4 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Maybe

Description

Definitions

import Stdlib.Data.Maybe.Base open public

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

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

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

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

\ No newline at end of file diff --git a/Stdlib.Data.Nat-src.html b/Stdlib.Data.Nat-src.html index 5ee0fada..df1398bd 100644 --- a/Stdlib.Data.Nat-src.html +++ b/Stdlib.Data.Nat-src.html @@ -43,4 +43,4 @@ mod := Nat.mod; fromNat (x : Nat) : Nat := x }; -Last modified on 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Data.Nat.Base-src.html b/Stdlib.Data.Nat.Base-src.html index 86541ebf..73d74df2 100644 --- a/Stdlib.Data.Nat.Base-src.html +++ b/Stdlib.Data.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 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Data.Nat.Base.html b/Stdlib.Data.Nat.Base.html index 1aca640a..9ff5816a 100644 --- a/Stdlib.Data.Nat.Base.html +++ b/Stdlib.Data.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/Stdlib.Data.Nat.Ord-src.html b/Stdlib.Data.Nat.Ord-src.html index a43b798f..59dc8bff 100644 --- a/Stdlib.Data.Nat.Ord-src.html +++ b/Stdlib.Data.Nat.Ord-src.html @@ -56,4 +56,4 @@ --- Returns the larger ;Nat;. max (x y : Nat) : Nat := if (x > y) x y; -Last modified on 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Data.Nat.Ord.html b/Stdlib.Data.Nat.Ord.html index 9a2860a2..456bd52f 100644 --- a/Stdlib.Data.Nat.Ord.html +++ b/Stdlib.Data.Nat.Ord.html @@ -2,4 +2,4 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Nat.Ord

Description

Definitions

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

Tests for equality.

/= (x y : Nat) : BoolSource#

Tests for inequality.

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

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

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

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

> (n m : Nat) : BoolSource#

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

>= (n m : Nat) : BoolSource#

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

compare (n m : Nat) : OrderingSource#

Tests for Ordering.

min (x y : Nat) : NatSource#

Returns the smaller Nat.

max (x y : Nat) : NatSource#

Returns the larger Nat.

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

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

> (n m : Nat) : BoolSource#

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

>= (n m : Nat) : BoolSource#

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

compare (n m : Nat) : OrderingSource#

Tests for Ordering.

min (x y : Nat) : NatSource#

Returns the smaller Nat.

max (x y : Nat) : NatSource#

Returns the larger Nat.

\ No newline at end of file diff --git a/Stdlib.Data.Nat.html b/Stdlib.Data.Nat.html index 8c9b3783..0ea87f19 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 -naturalNatI : Natural NatSource#

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

\ No newline at end of file diff --git a/Stdlib.Data.Product-src.html b/Stdlib.Data.Product-src.html index 06a80435..58045a5a 100644 --- a/Stdlib.Data.Product-src.html +++ b/Stdlib.Data.Product-src.html @@ -30,4 +30,4 @@ | {{mkShow show-a}} {{mkShow show-b}} := mkShow λ {(a, b) := "(" ++str show-a a ++str " , " ++str show-b b ++str ")"}; -Last modified on 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Data.Product.Base-src.html b/Stdlib.Data.Product.Base-src.html index e0feb1ec..03d20056 100644 --- a/Stdlib.Data.Product.Base-src.html +++ b/Stdlib.Data.Product.Base-src.html @@ -39,4 +39,4 @@ --- Applies a function to both components. both {A B} (f : A → B) : A × A → B × B | (a, b) := f a, f b; -Last modified on 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Data.Product.Base.html b/Stdlib.Data.Product.Base.html index 125146f8..245f5f81 100644 --- a/Stdlib.Data.Product.Base.html +++ b/Stdlib.Data.Product.Base.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Product.Base

Description

Definitions

type × (A B : Type)Source#

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

Constructors

| , : A → B → A × B

uncurry {A B C} (f : A -> B -> C) : A × B -> CSource#

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

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

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

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

Projects the first component of a tuple.

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

Projects the second component of a tuple.

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

Swaps the components of a tuple.

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

Applies a function to the first component.

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

Applies a function to the second component.

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

Applies a function to both components.

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

Stdlib.Data.Product.Base

Description

Definitions

type × (A B : Type)Source#

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

Constructors

| , : A → B → A × B

uncurry {A B C} (f : A -> B -> C) : A × B -> CSource#

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

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

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

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

Projects the first component of a tuple.

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

Projects the second component of a tuple.

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

Swaps the components of a tuple.

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

Applies a function to the first component.

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

Applies a function to the second component.

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

Applies a function to both components.

\ No newline at end of file diff --git a/Stdlib.Data.Product.html b/Stdlib.Data.Product.html index 4c4e2169..85e2f538 100644 --- a/Stdlib.Data.Product.html +++ b/Stdlib.Data.Product.html @@ -2,4 +2,4 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Product

Description

Definitions

import Stdlib.Data.Product.Base open public

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

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

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

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

\ No newline at end of file diff --git a/Stdlib.Data.String-src.html b/Stdlib.Data.String-src.html index baece884..82be1db9 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 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Data.String.Base-src.html b/Stdlib.Data.String.Base-src.html index 45c35a6d..9fb4dd9c 100644 --- a/Stdlib.Data.String.Base-src.html +++ b/Stdlib.Data.String.Base-src.html @@ -19,4 +19,4 @@ --- Joins a ;List; of ;String;s with "\n". unlines : List String -> String := concatStr ∘ intersperse "\n"; -Last modified on 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Data.String.Base.html b/Stdlib.Data.String.Base.html index 255c9aa9..c54fdd8c 100644 --- a/Stdlib.Data.String.Base.html +++ b/Stdlib.Data.String.Base.html @@ -1,4 +1,4 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.String.Base

Description

Definitions

builtin string axiom String : TypeSource#

Primitive representation of a sequence of characters.

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

Concatenation of two Strings.

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 +axiom ++str : String -> String -> StringSource#

Concatenation of two Strings.

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 94d94225..e8173af6 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 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Data.String.Ord.html b/Stdlib.Data.String.Ord.html index b5815314..99b49bc4 100644 --- a/Stdlib.Data.String.Ord.html +++ b/Stdlib.Data.String.Ord.html @@ -1,3 +1,3 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.String.Ord

Description

Definitions

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

Equality for Strings.

\ No newline at end of file +axiom == : String → String → BoolSource#

Equality for Strings.

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

Stdlib.Data.String

Description

Definitions

import Stdlib.Data.String.Base open public

instance eqStringI : Eq StringSource#

instance -showStringI : Show StringSource#

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

\ No newline at end of file diff --git a/Stdlib.Data.Unit-src.html b/Stdlib.Data.Unit-src.html index aa0de1b9..0e87ecce 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 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Data.Unit.html b/Stdlib.Data.Unit.html index b9e33098..25a60b26 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 a26760d0..a899af39 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 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Debug.Fail.html b/Stdlib.Debug.Fail.html index ad8b4260..514444e3 100644 --- a/Stdlib.Debug.Fail.html +++ b/Stdlib.Debug.Fail.html @@ -1,3 +1,3 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Debug.Fail

Description

Definitions

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

Primitive that exits the program with an error message.

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

Primitive that exits the program with an error message.

\ No newline at end of file diff --git a/Stdlib.Function-src.html b/Stdlib.Function-src.html index a33345f3..ac58d02f 100644 --- a/Stdlib.Function-src.html +++ b/Stdlib.Function-src.html @@ -43,4 +43,4 @@ builtin seq >>> : {A B : Type} → A → B → B | x y := y; -Last modified on 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Function.html b/Stdlib.Function.html index 1b3ca3c7..19e2f578 100644 --- a/Stdlib.Function.html +++ b/Stdlib.Function.html @@ -1,3 +1,3 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Function

Description

Definitions

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

Function composition.

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.

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 ca94c692..8c0df2bb 100644 --- a/Stdlib.Prelude-src.html +++ b/Stdlib.Prelude-src.html @@ -16,4 +16,4 @@ import Stdlib.System.IO open public; import Stdlib.Trait open public; -Last modified on 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Prelude.html b/Stdlib.Prelude.html index 9a505b02..6c7b829e 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.Product 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.Product 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 diff --git a/Stdlib.System.IO-src.html b/Stdlib.System.IO-src.html index 0bd64502..4bdd9a36 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 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.System.IO.Base-src.html b/Stdlib.System.IO.Base-src.html index f3d79ac6..893f2f66 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 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.System.IO.Base.html b/Stdlib.System.IO.Base.html index 4bd2fc38..11be93a5 100644 --- a/Stdlib.System.IO.Base.html +++ b/Stdlib.System.IO.Base.html @@ -1,4 +1,4 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.System.IO.Base

Description

Definitions

builtin IO axiom IO : TypeSource#

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

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

\ No newline at end of file diff --git a/Stdlib.System.IO.Bool-src.html b/Stdlib.System.IO.Bool-src.html index a52ad427..cb37a32c 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 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.System.IO.Bool.html b/Stdlib.System.IO.Bool.html index 16d675f4..809a6c0a 100644 --- a/Stdlib.System.IO.Bool.html +++ b/Stdlib.System.IO.Bool.html @@ -1,3 +1,3 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.System.IO.Bool

Description

Definitions

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

printBoolLn (b : Bool) : IOSource#

\ No newline at end of file +axiom printBool : Bool → IOSource#

printBoolLn (b : Bool) : IOSource#

\ No newline at end of file diff --git a/Stdlib.System.IO.Int-src.html b/Stdlib.System.IO.Int-src.html index cec7c065..8ae14fbe 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 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.System.IO.Int.html b/Stdlib.System.IO.Int.html index f01b3e08..eed64002 100644 --- a/Stdlib.System.IO.Int.html +++ b/Stdlib.System.IO.Int.html @@ -1,3 +1,3 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.System.IO.Int

Description

Definitions

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

printIntLn (i : Int) : IOSource#

\ No newline at end of file +axiom printInt : Int → IOSource#

printIntLn (i : Int) : IOSource#

\ No newline at end of file diff --git a/Stdlib.System.IO.Nat-src.html b/Stdlib.System.IO.Nat-src.html index f5dd72cf..6d24d9dd 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 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.System.IO.Nat.html b/Stdlib.System.IO.Nat.html index 979de400..41d99c43 100644 --- a/Stdlib.System.IO.Nat.html +++ b/Stdlib.System.IO.Nat.html @@ -1,3 +1,3 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.System.IO.Nat

Description

Definitions

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

printNatLn (n : Nat) : IOSource#

\ No newline at end of file +axiom printNat : Nat → IOSource#

printNatLn (n : Nat) : IOSource#

\ No newline at end of file diff --git a/Stdlib.System.IO.String-src.html b/Stdlib.System.IO.String-src.html index b8372019..bc503e0c 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 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.System.IO.String.html b/Stdlib.System.IO.String.html index 01756eca..7d37e237 100644 --- a/Stdlib.System.IO.String.html +++ b/Stdlib.System.IO.String.html @@ -1,4 +1,4 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.System.IO.String

Description

Definitions

builtin string-print axiom printString : String → IOSource#

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

printStringLn (s : String) : IOSource#

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

printStringLn (s : String) : IOSource#

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

Stdlib.System.IO

Description

Definitions

import Stdlib.System.IO.Base open public

import Stdlib.System.IO.Bool open public

import Stdlib.System.IO.Nat open public

import Stdlib.System.IO.Int open public

import Stdlib.System.IO.String open public

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

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

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

Stdlib.System.IO

Description

Definitions

import Stdlib.System.IO.Base open public

import Stdlib.System.IO.Bool open public

import Stdlib.System.IO.Nat open public

import Stdlib.System.IO.Int open public

import Stdlib.System.IO.String open public

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

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

\ No newline at end of file diff --git a/Stdlib.Trait-src.html b/Stdlib.Trait-src.html index 62ac6965..06425b65 100644 --- a/Stdlib.Trait-src.html +++ b/Stdlib.Trait-src.html @@ -7,4 +7,4 @@ import Stdlib.Trait.Partial open public; import Stdlib.Trait.Natural open public; import Stdlib.Trait.Integral open public; -Last modified on 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Eq-src.html b/Stdlib.Trait.Eq-src.html index 0e3e24e0..6e0f31e3 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 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Eq.html b/Stdlib.Trait.Eq.html index 1a1c701c..6dcef140 100644 --- a/Stdlib.Trait.Eq.html +++ b/Stdlib.Trait.Eq.html @@ -1,3 +1,3 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Eq

Description

Definitions

trait -type Eq ASource#

A trait defining equality

Constructors

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

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

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

Tests for inequality.

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

A trait defining equality

Constructors

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

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

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

Tests for inequality.

\ No newline at end of file diff --git a/Stdlib.Trait.Integral-src.html b/Stdlib.Trait.Integral-src.html index b1dc4f8a..a11c08e1 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 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Integral.html b/Stdlib.Trait.Integral.html index 404bbd66..3ce29721 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 c91bda3e..5df6d32f 100644 --- a/Stdlib.Trait.Natural-src.html +++ b/Stdlib.Trait.Natural-src.html @@ -18,4 +18,4 @@ }; open Natural public; -Last modified on 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Natural.html b/Stdlib.Trait.Natural.html index 630116ea..16875120 100644 --- a/Stdlib.Trait.Natural.html +++ b/Stdlib.Trait.Natural.html @@ -9,4 +9,4 @@ mod : 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.Trait.Ord-src.html b/Stdlib.Trait.Ord-src.html index 9b5d651a..06da222b 100644 --- a/Stdlib.Trait.Ord-src.html +++ b/Stdlib.Trait.Ord-src.html @@ -76,4 +76,4 @@ --- Returns the larger element. {-# inline: always #-} max {A} {{Ord A}} (x y : A) : A := if (x > y) x y; -Last modified on 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Ord.html b/Stdlib.Trait.Ord.html index 6fab6c23..777cb29d 100644 --- a/Stdlib.Trait.Ord.html +++ b/Stdlib.Trait.Ord.html @@ -1,4 +1,4 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Ord

Description

Definitions

type OrderingSource#

Constructors

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

isLT : Ordering → BoolSource#

isEQ : Ordering → BoolSource#

isGT : Ordering → BoolSource#

instance orderingEqI : Eq OrderingSource#

trait -type Ord ASource#

A trait for defining a total order

Constructors

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

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

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

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

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

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

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

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

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

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

Returns the smaller element.

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

Returns the larger element.

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

A trait for defining a total order

Constructors

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

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

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

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

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

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

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

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

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

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

Returns the smaller element.

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

Returns the larger element.

\ No newline at end of file diff --git a/Stdlib.Trait.Partial-src.html b/Stdlib.Trait.Partial-src.html index 04aead26..9bc66e0a 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 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Partial.html b/Stdlib.Trait.Partial.html index b0e498a8..a92dd8b4 100644 --- a/Stdlib.Trait.Partial.html +++ b/Stdlib.Trait.Partial.html @@ -1,3 +1,3 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Partial

Description

Definitions

trait -type PartialSource#

Constructors

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

open Partial public

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

\ No newline at end of file +type PartialSource#

Constructors

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

open Partial public

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

\ No newline at end of file diff --git a/Stdlib.Trait.Show-src.html b/Stdlib.Trait.Show-src.html index 7c319dc5..9a78332e 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 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/Stdlib.Trait.Show.html b/Stdlib.Trait.Show.html index 7af024f4..c62f2fd3 100644 --- a/Stdlib.Trait.Show.html +++ b/Stdlib.Trait.Show.html @@ -1,3 +1,3 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Show

Description

Definitions

trait -type Show ASource#

Constructors

| mkShow {show : A -> String}
\ No newline at end of file +type Show ASource#

Constructors

| mkShow {show : A -> String}
\ No newline at end of file diff --git a/Stdlib.Trait.html b/Stdlib.Trait.html index a0698c51..63568698 100644 --- a/Stdlib.Trait.html +++ b/Stdlib.Trait.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait

Description

Definitions

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

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

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

import Stdlib.Trait.Partial open public

import Stdlib.Trait.Natural open public

import Stdlib.Trait.Integral open public

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

Stdlib.Trait

Description

Definitions

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

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

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

import Stdlib.Trait.Partial open public

import Stdlib.Trait.Natural open public

import Stdlib.Trait.Integral open public

\ No newline at end of file diff --git a/index-src.html b/index-src.html index 628553be..7c63067e 100644 --- a/index-src.html +++ b/index-src.html @@ -14,4 +14,4 @@ import Stdlib.Data.Nat.Ord; import Stdlib.Data.Int.Ord; import Stdlib.Data.String.Ord; -Last modified on 2023-11-20 3:25 UTC \ No newline at end of file +Last modified on 2023-11-27 3:15 UTC \ No newline at end of file diff --git a/index.html b/index.html index 8b0fc5f5..051ab269 100644 --- a/index.html +++ b/index.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Modules

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

Modules

\ No newline at end of file