From 2fb46165e8c6865a7b6fff94d22fe30e681d7ccc Mon Sep 17 00:00:00 2001 From: paulcadman Date: Wed, 14 Aug 2024 15:20:23 +0000 Subject: [PATCH] deploy: 17a82dd466010b51924677b16a3f09a6c4c86a80 --- 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.FromNatural-src.html | 2 +- Juvix.Builtin.V1.Trait.FromNatural.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 | 4 +- Stdlib.Data.Bool.Base-src.html | 4 +- Stdlib.Data.Bool.Base.html | 2 +- Stdlib.Data.Bool.html | 2 +- Stdlib.Data.Byte-src.html | 2 +- Stdlib.Data.Byte.Base-src.html | 2 +- Stdlib.Data.Byte.Base.html | 2 +- Stdlib.Data.Byte.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 | 6 +- Stdlib.Data.List.Base-src.html | 2 +- Stdlib.Data.List.Base.html | 2 +- Stdlib.Data.List.html | 2 +- Stdlib.Data.Maybe-src.html | 6 +- 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 | 4 +- Stdlib.Data.Pair.Base-src.html | 2 +- Stdlib.Data.Pair.Base.html | 2 +- Stdlib.Data.Pair.html | 2 +- Stdlib.Data.Range-src.html | 94 +++++++++++++++++++++ Stdlib.Data.Range.html | 10 +++ Stdlib.Data.Result-src.html | 6 +- Stdlib.Data.Result.Base-src.html | 2 +- Stdlib.Data.Result.Base.html | 2 +- Stdlib.Data.Result.html | 2 +- Stdlib.Data.String-src.html | 2 +- Stdlib.Data.String.Base-src.html | 2 +- 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 | 5 +- 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 | 4 +- Stdlib.Trait.Eq.html | 2 +- Stdlib.Trait.Foldable-src.html | 2 +- Stdlib.Trait.Foldable.Monomorphic-src.html | 12 +-- Stdlib.Trait.Foldable.Monomorphic.html | 4 +- Stdlib.Trait.Foldable.Polymorphic-src.html | 6 +- Stdlib.Trait.Foldable.Polymorphic.html | 4 +- Stdlib.Trait.Foldable.html | 2 +- Stdlib.Trait.FromNatural-src.html | 2 +- Stdlib.Trait.FromNatural.html | 2 +- Stdlib.Trait.Functor-src.html | 2 +- Stdlib.Trait.Functor.Monomorphic-src.html | 11 ++- Stdlib.Trait.Functor.Monomorphic.html | 3 +- Stdlib.Trait.Functor.Polymorphic-src.html | 11 ++- Stdlib.Trait.Functor.Polymorphic.html | 3 +- Stdlib.Trait.Functor.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 | 6 +- 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 +- 124 files changed, 274 insertions(+), 140 deletions(-) create mode 100644 Stdlib.Data.Range-src.html create mode 100644 Stdlib.Data.Range.html diff --git a/Juvix.Builtin.V1.Bool-src.html b/Juvix.Builtin.V1.Bool-src.html index 77084bde..d93ecc59 100644 --- a/Juvix.Builtin.V1.Bool-src.html +++ b/Juvix.Builtin.V1.Bool-src.html @@ -6,4 +6,4 @@ type Bool := | true | false; - \ No newline at end of file + \ No newline at end of file diff --git a/Juvix.Builtin.V1.Bool.html b/Juvix.Builtin.V1.Bool.html index 0785ee7a..e2886053 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 72ecff96..c86a70c3 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]}; - \ No newline at end of file + \ No newline at end of file diff --git a/Juvix.Builtin.V1.Fixity.html b/Juvix.Builtin.V1.Fixity.html index 1469f34b..c036aa5c 100644 --- a/Juvix.Builtin.V1.Fixity.html +++ b/Juvix.Builtin.V1.Fixity.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Juvix.Builtin.V1.Fixity

Definitions

syntax fixity noneSource#

Fixity details

none

syntax fixity rappSource#

Fixity details

binary; right-associative

syntax fixity lappSource#

Fixity details

binary; left-associative
Same precedence as rapp

syntax fixity seqSource#

Fixity details

binary; left-associative
Higher precedence than: lapp

syntax fixity functorSource#

Fixity details

binary; right-associative

syntax fixity logicalSource#

Fixity details

binary; right-associative
Higher precedence than: seq

syntax fixity comparisonSource#

Fixity details

binary
Higher precedence than: logical

syntax fixity pairSource#

Fixity details

binary; right-associative

syntax fixity consSource#

Fixity details

binary; right-associative
Higher precedence than: pair

syntax fixity stepSource#

Fixity details

binary; right-associative

syntax fixity rangeSource#

Fixity details

binary; right-associative
Higher precedence than: step

syntax fixity additiveSource#

Fixity details

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

syntax fixity multiplicativeSource#

Fixity details

binary; left-associative
Higher precedence than: additive

syntax fixity compositionSource#

Fixity details

binary; right-associative
Higher precedence than: multiplicative

syntax fixity lcompositionSource#

Fixity details

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

Juvix.Builtin.V1.Fixity

Definitions

syntax fixity noneSource#

Fixity details

none

syntax fixity rappSource#

Fixity details

binary; right-associative

syntax fixity lappSource#

Fixity details

binary; left-associative
Same precedence as rapp

syntax fixity seqSource#

Fixity details

binary; left-associative
Higher precedence than: lapp

syntax fixity functorSource#

Fixity details

binary; right-associative

syntax fixity logicalSource#

Fixity details

binary; right-associative
Higher precedence than: seq

syntax fixity comparisonSource#

Fixity details

binary
Higher precedence than: logical

syntax fixity pairSource#

Fixity details

binary; right-associative

syntax fixity consSource#

Fixity details

binary; right-associative
Higher precedence than: pair

syntax fixity stepSource#

Fixity details

binary; right-associative

syntax fixity rangeSource#

Fixity details

binary; right-associative
Higher precedence than: step

syntax fixity additiveSource#

Fixity details

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

syntax fixity multiplicativeSource#

Fixity details

binary; left-associative
Higher precedence than: additive

syntax fixity compositionSource#

Fixity details

binary; right-associative
Higher precedence than: multiplicative

syntax fixity lcompositionSource#

Fixity details

binary; left-associative
Higher precedence than: multiplicative
\ No newline at end of file diff --git a/Juvix.Builtin.V1.List-src.html b/Juvix.Builtin.V1.List-src.html index fdd6ae98..c6437ad2 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); - \ No newline at end of file + \ No newline at end of file diff --git a/Juvix.Builtin.V1.List.html b/Juvix.Builtin.V1.List.html index 0e50f3c3..e47d9137 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 bbac4b3c..b77f10c9 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; - \ No newline at end of file + \ No newline at end of file diff --git a/Juvix.Builtin.V1.Maybe.html b/Juvix.Builtin.V1.Maybe.html index 77590621..c5c80f1e 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 921cf42d..28ac9442 100644 --- a/Juvix.Builtin.V1.Nat-src.html +++ b/Juvix.Builtin.V1.Nat-src.html @@ -20,4 +20,4 @@ + := (Nat.+); * := (Nat.*) }; - \ No newline at end of file + \ No newline at end of file diff --git a/Juvix.Builtin.V1.Nat.Base-src.html b/Juvix.Builtin.V1.Nat.Base-src.html index 46f64cec..6bf4edfe 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); - \ No newline at end of file + \ No newline at end of file diff --git a/Juvix.Builtin.V1.Nat.Base.html b/Juvix.Builtin.V1.Nat.Base.html index 30fe742e..e432e7c9 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 a4dbd333..31f1a480 100644 --- a/Juvix.Builtin.V1.Nat.html +++ b/Juvix.Builtin.V1.Nat.html @@ -1,4 +1,4 @@ Juvix Documentation
stdlib - 0.0.1

Juvix.Builtin.V1.Nat

\ 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 165f888a..99a79b48 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; - \ No newline at end of file + \ No newline at end of file diff --git a/Juvix.Builtin.V1.String.html b/Juvix.Builtin.V1.String.html index 6b678978..114847b0 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.FromNatural-src.html b/Juvix.Builtin.V1.Trait.FromNatural-src.html index d9144502..fc2565c5 100644 --- a/Juvix.Builtin.V1.Trait.FromNatural-src.html +++ b/Juvix.Builtin.V1.Trait.FromNatural-src.html @@ -7,4 +7,4 @@ type FromNatural A := mkFromNatural {builtin from-nat fromNat : Nat -> A}; open FromNatural public; - \ No newline at end of file + \ No newline at end of file diff --git a/Juvix.Builtin.V1.Trait.FromNatural.html b/Juvix.Builtin.V1.Trait.FromNatural.html index 3979e3d6..ece2acbe 100644 --- a/Juvix.Builtin.V1.Trait.FromNatural.html +++ b/Juvix.Builtin.V1.Trait.FromNatural.html @@ -1,4 +1,4 @@ Juvix Documentation
stdlib - 0.0.1

Juvix.Builtin.V1.Trait.FromNatural

Definitions

trait type FromNatural ASource#

Constructors

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

open FromNatural public

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

open FromNatural public

\ No newline at end of file diff --git a/Juvix.Builtin.V1.Trait.Natural-src.html b/Juvix.Builtin.V1.Trait.Natural-src.html index 3ca46065..f1e8f8db 100644 --- a/Juvix.Builtin.V1.Trait.Natural-src.html +++ b/Juvix.Builtin.V1.Trait.Natural-src.html @@ -18,4 +18,4 @@ }; open Natural public; - \ No newline at end of file + \ No newline at end of file diff --git a/Juvix.Builtin.V1.Trait.Natural.html b/Juvix.Builtin.V1.Trait.Natural.html index ab24642d..d55ecdf5 100644 --- a/Juvix.Builtin.V1.Trait.Natural.html +++ b/Juvix.Builtin.V1.Trait.Natural.html @@ -8,4 +8,4 @@ syntax operator * multiplicative; {-# isabelle-operator: {name: "*", prec: 70, assoc: left} #-} * : A -> A -> A - }

open Natural public

\ No newline at end of file + }

open Natural public

\ No newline at end of file diff --git a/Stdlib.Cairo.Poseidon-src.html b/Stdlib.Cairo.Poseidon-src.html index b7bee84c..9dd2d1a4 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); - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Cairo.Poseidon.html b/Stdlib.Cairo.Poseidon.html index 10415a17..c61e8e44 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 f225c74c..d207764f 100644 --- a/Stdlib.Data.Bool-src.html +++ b/Stdlib.Data.Bool-src.html @@ -6,6 +6,7 @@ import Stdlib.Trait.Ord open; import Stdlib.Trait.Show open; +{-# specialize: true, inline: case #-} instance boolEqI : Eq Bool := mkEq @@ -15,6 +16,7 @@ | _ _ := false }; +{-# specialize: true, inline: case #-} instance boolOrdI : Ord Bool := mkOrd @@ -32,4 +34,4 @@ | true := "true" | false := "false" }; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Data.Bool.Base-src.html b/Stdlib.Data.Bool.Base-src.html index a61dec15..c5583021 100644 --- a/Stdlib.Data.Bool.Base-src.html +++ b/Stdlib.Data.Bool.Base-src.html @@ -5,7 +5,7 @@ import Stdlib.Data.Fixity open; --- Logical negation. -{-# isabelle-function: {name: "¬"} #-} +{-# isabelle-function: {name: "\\<not>"} #-} not : Bool → Bool | true := false | false := true; @@ -37,4 +37,4 @@ --- Logical conjunction. and (a b : Bool) : Bool := a && b; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Data.Bool.Base.html b/Stdlib.Data.Bool.Base.html index 9f677ba2..4b91f27f 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 b0d6d2f5..aaa2746b 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.Byte-src.html b/Stdlib.Data.Byte-src.html index 56c05eaa..7a779780 100644 --- a/Stdlib.Data.Byte-src.html +++ b/Stdlib.Data.Byte-src.html @@ -27,4 +27,4 @@ mkFromNatural@{ fromNat := Byte.fromNat }; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Data.Byte.Base-src.html b/Stdlib.Data.Byte.Base-src.html index 39482294..1e222ff6 100644 --- a/Stdlib.Data.Byte.Base-src.html +++ b/Stdlib.Data.Byte.Base-src.html @@ -21,4 +21,4 @@ builtin byte-eq axiom == : Byte -> Byte -> Bool; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Data.Byte.Base.html b/Stdlib.Data.Byte.Base.html index 9a595712..c4ded7de 100644 --- a/Stdlib.Data.Byte.Base.html +++ b/Stdlib.Data.Byte.Base.html @@ -3,4 +3,4 @@ axiom Byte : TypeSource#

An 8-bit unsigned integer.

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

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

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

Converts a Byte to the corresponding Nat.

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

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

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

Stdlib.Data.Byte

Definitions

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

import Stdlib.Data.Byte.Base as Byte public

import Stdlib.Trait.Eq open public

import Stdlib.Trait.Show open public

instance eqByteI : Eq ByteSource#

instance showByteI : Show ByteSource#

instance -fromNaturalByteI : FromNatural ByteSource#

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

\ No newline at end of file diff --git a/Stdlib.Data.Field-src.html b/Stdlib.Data.Field-src.html index eaaad61e..636d2d15 100644 --- a/Stdlib.Data.Field-src.html +++ b/Stdlib.Data.Field-src.html @@ -54,4 +54,4 @@ integralI := integralFieldI; / := (Field./) }; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Data.Field.Base-src.html b/Stdlib.Data.Field.Base-src.html index 8c51f08a..436ecc60 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); - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Data.Field.Base.html b/Stdlib.Data.Field.Base.html index dd4a396a..eee037fc 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 4ef03ad6..2a56dd71 100644 --- a/Stdlib.Data.Field.html +++ b/Stdlib.Data.Field.html @@ -5,4 +5,4 @@ fromNaturalFieldI : FromNatural 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 75527a93..36ba3251 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;
-
\ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Data.Fixity.html b/Stdlib.Data.Fixity.html index eaec0d0c..515220d2 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 38a49934..1c2d4326 100644 --- a/Stdlib.Data.Int-src.html +++ b/Stdlib.Data.Int-src.html @@ -65,4 +65,4 @@ div := Int.div; mod := Int.mod }; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Data.Int.Base-src.html b/Stdlib.Data.Int.Base-src.html index 08fffed2..1eab1920 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; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Data.Int.Base.html b/Stdlib.Data.Int.Base.html index bfc10931..372d3353 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 4271d620..d6cd6940 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; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Data.Int.Ord.html b/Stdlib.Data.Int.Ord.html index bf42a044..718d82e2 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 fc50816a..634d9353 100644 --- a/Stdlib.Data.Int.html +++ b/Stdlib.Data.Int.html @@ -7,4 +7,4 @@ fromNaturalIntI : FromNatural IntSource#

instance naturalIntI : Natural IntSource#

instance integralIntI : Integral IntSource#

instance -divModIntI : DivMod IntSource#

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

\ No newline at end of file diff --git a/Stdlib.Data.List-src.html b/Stdlib.Data.List-src.html index 68ae2fb7..7bd3bed7 100644 --- a/Stdlib.Data.List-src.html +++ b/Stdlib.Data.List-src.html @@ -54,16 +54,19 @@ | s := "(" ++str go s ++str ")" }; +{-# specialize: true, inline: case #-} instance functorListI : Functor List := mkFunctor@{ map := listMap }; +{-# specialize: true, inline: true #-} instance monomorphicFunctorListI {A} : Monomorphic.Functor (List A) A := fromPolymorphicFunctor; +{-# specialize: true, inline: case #-} instance polymorphicFoldableListI : Polymorphic.Foldable List := Polymorphic.mkFoldable@{ @@ -71,6 +74,7 @@ rfor := listRfor }; +{-# specialize: true, inline: true #-} instance foldableListI {A} : Foldable (List A) A := fromPolymorphicFoldable; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Data.List.Base-src.html b/Stdlib.Data.List.Base-src.html index 695b1d66..c177411c 100644 --- a/Stdlib.Data.List.Base-src.html +++ b/Stdlib.Data.List.Base-src.html @@ -231,4 +231,4 @@ | nil := nil | (xs :: nil) := listMap λ {x := x :: nil} xs | (xs :: xss) := zipWith (::) xs (transpose xss); - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Data.List.Base.html b/Stdlib.Data.List.Base.html index b8176b9f..25f12084 100644 --- a/Stdlib.Data.List.Base.html +++ b/Stdlib.Data.List.Base.html @@ -1,4 +1,4 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.List.Base

Definitions

import Juvix.Builtin.V1.List open public

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

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

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

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

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

Right-associative fold.

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

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

Left-associative and tail-recursive fold.

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

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

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

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

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

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

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

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

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

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

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

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

Takes the first n elements of a List.

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

Drops the first n elements of a List.

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

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

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

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

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

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

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

Concatenates two Lists.

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

𝒪(𝓃). Append an element.

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

Concatenates a List of Lists.

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

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

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

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

tail {A} : List A → List ASource#

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

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

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

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

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

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

null {A} : List A → BoolSource#

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\ No newline at end of file +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 694bbe90..f7394551 100644 --- a/Stdlib.Data.List.html +++ b/Stdlib.Data.List.html @@ -6,4 +6,4 @@ functorListI : Functor ListSource#

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

instance polymorphicFoldableListI : Polymorphic.Foldable ListSource#

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

\ No newline at end of file +foldableListI {A} : Foldable (List A) ASource#

\ No newline at end of file diff --git a/Stdlib.Data.Maybe-src.html b/Stdlib.Data.Maybe-src.html index 00b0d7c5..0cff5cf2 100644 --- a/Stdlib.Data.Maybe-src.html +++ b/Stdlib.Data.Maybe-src.html @@ -11,6 +11,7 @@ import Stdlib.Data.Bool.Base open; import Stdlib.Data.String.Base open; +{-# specialize: true, inline: case #-} instance eqMaybeI {A} {{Eq A}} : Eq (Maybe A) := mkEq @@ -28,6 +29,7 @@ | (just a) := "just " ++str Show.show a }; +{-# specialize: true, inline: case #-} instance ordMaybeI {A} {{Ord A}} : Ord (Maybe A) := mkOrd @@ -38,6 +40,7 @@ | (just _) nothing := GT }; +{-# specialize: true, inline: case #-} instance functorMaybeI : Functor Maybe := mkFunctor@{ @@ -46,7 +49,8 @@ | (just a) := just (f a) }; +{-# specizalize: true, inline: true #-} instance monomorphicFunctorMaybeI {A} : Monomorphic.Functor (Maybe A) A := fromPolymorphicFunctor; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Data.Maybe.Base-src.html b/Stdlib.Data.Maybe.Base-src.html index 5ef9bb7b..5d7e9981 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; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Data.Maybe.Base.html b/Stdlib.Data.Maybe.Base.html index e390d902..298da193 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 ac5e4a00..6ec4b052 100644 --- a/Stdlib.Data.Maybe.html +++ b/Stdlib.Data.Maybe.html @@ -4,4 +4,4 @@ showMaybeI {A} {{Show A}} : Show (Maybe A)Source#

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

instance functorMaybeI : Functor MaybeSource#

instance -monomorphicFunctorMaybeI {A} : Monomorphic.Functor (Maybe A) ASource#

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

\ No newline at end of file diff --git a/Stdlib.Data.Nat-src.html b/Stdlib.Data.Nat-src.html index 3782e2f4..6613ae2b 100644 --- a/Stdlib.Data.Nat-src.html +++ b/Stdlib.Data.Nat-src.html @@ -43,4 +43,4 @@ div := Nat.div; mod := Nat.mod }; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Data.Nat.Base-src.html b/Stdlib.Data.Nat.Base-src.html index ef8bf3c6..157c6e31 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;
-
\ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Data.Nat.Base.html b/Stdlib.Data.Nat.Base.html index e36dc6ee..f1710985 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 0a717a25..8b02a842 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; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Data.Nat.Ord.html b/Stdlib.Data.Nat.Ord.html index 9a59e508..087b076c 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 59953f53..c17a9b01 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 79c49999..9c9c616b 100644 --- a/Stdlib.Data.Pair-src.html +++ b/Stdlib.Data.Pair-src.html @@ -9,11 +9,13 @@ import Stdlib.Trait.Ord open; import Stdlib.Trait.Show open; +{-# specialize: true, inline: case #-} instance eqProductI {A B} : {{Eq A}} -> {{Eq B}} -> Eq (Pair A B) | {{mkEq eq-a}} {{mkEq eq-b}} := mkEq λ {(a1, b1) (a2, b2) := eq-a a1 a2 && eq-b b1 b2}; +{-# specialize: true, inline: case #-} instance ordProductI {A B} : {{Ord A}} -> {{Ord B}} -> Ord (Pair A B) | {{mkOrd cmp-a}} {{mkOrd cmp-b}} := @@ -29,4 +31,4 @@ | {{mkShow show-a}} {{mkShow show-b}} := mkShow λ {(a, b) := "(" ++str show-a a ++str " , " ++str show-b b ++str ")"}; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Data.Pair.Base-src.html b/Stdlib.Data.Pair.Base-src.html index 7989c08d..13ac2b9d 100644 --- a/Stdlib.Data.Pair.Base-src.html +++ b/Stdlib.Data.Pair.Base-src.html @@ -39,4 +39,4 @@ --- Applies a function to both components. both {A B} (f : A → B) : Pair A A → Pair B B | (a, b) := f a, f b; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Data.Pair.Base.html b/Stdlib.Data.Pair.Base.html index dfce5390..e8d062ca 100644 --- a/Stdlib.Data.Pair.Base.html +++ b/Stdlib.Data.Pair.Base.html @@ -1,3 +1,3 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Pair.Base

Definitions

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

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

Constructors

| , : A → B → Pair A B

uncurry {A B C} (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 +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 07af55a2..6732d0f3 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.Range-src.html b/Stdlib.Data.Range-src.html new file mode 100644 index 00000000..4e6ade9a --- /dev/null +++ b/Stdlib.Data.Range-src.html @@ -0,0 +1,94 @@ + +
module Stdlib.Data.Range;
+
+import Stdlib.Data.Fixity open;
+
+import Stdlib.Data.Bool.Base open;
+import Stdlib.Trait.Natural open;
+import Stdlib.Trait.Ord open;
+import Stdlib.Trait.Foldable open;
+import Stdlib.Data.Nat open;
+
+--- An inclusive range of naturals
+type Range N :=
+  mkRange {
+    low : N;
+    high : N
+  };
+
+type StepRange N :=
+  mkStepRange {
+    range : Range N;
+    step : N
+  };
+
+syntax operator to range;
+
+--- `x to y` is the range [x..y]
+{-# inline: always #-}
+to {N} {{Natural N}} (l h : N) : Range N := mkRange l h;
+
+syntax operator step step;
+
+--- `x to y step s` is the range [x, x + s, ..., y]
+{-# inline: always #-}
+step {N} (r : Range N) (s : N) : StepRange N := mkStepRange r s;
+
+-- This instance assumes that `low <= high`.
+{-# specialize: true, inline: case #-}
+instance
+foldableRangeI {N} {{Eq N}} {{Natural N}} : Foldable (Range N) N :=
+  mkFoldable@{
+    {-# specialize: [1, 3] #-}
+    for {B : Type} (f : B -> N -> B) (ini : B) : Range N -> B
+      | (mkRange low high) :=
+        let
+          {-# specialize-by: [f, high] #-}
+          terminating
+          go (acc : B) (next : N) : B :=
+            if 
+              | next == high := f acc next
+              | else := go (f acc next) (next + 1);
+        in go ini low;
+    {-# specialize: [1, 3] #-}
+    rfor {B : Type} (f : B -> N -> B) (ini : B) : Range N -> B
+      | (mkRange low high) :=
+        let
+          {-# specialize-by: [f, high] #-}
+          terminating
+          go (next : N) : B :=
+            if 
+              | next == high := f ini next
+              | else := f (go (next + 1)) next;
+        in go low
+  };
+
+-- This instance assumes that (low + step*k > high) for some k.
+{-# specialize: true, inline: case #-}
+instance
+foldableStepRangeI {N} {{Ord N}} {{Natural N}} : Foldable (StepRange N) N :=
+  mkFoldable@{
+    {-# specialize: [1, 3] #-}
+    for {B : Type} (f : B -> N -> B) (ini : B) : StepRange N -> B
+      | (mkStepRange (mkRange low high) step) :=
+        let
+          {-# specialize-by: [f, high, step] #-}
+          terminating
+          go (acc : B) (next : N) : B :=
+            if 
+              | next > high := acc
+              | else := go (f acc next) (next + step);
+        in go ini low;
+    {-# specialize: [1, 3] #-}
+    rfor {B : Type} (f : B -> N -> B) (ini : B) : StepRange N -> B
+      | (mkStepRange (mkRange low high) step) :=
+        let
+          {-# specialize-by: [f, high, step] #-}
+          terminating
+          go (next : N) : B :=
+            if 
+              | next <= high := f (go (next + step)) next
+              | else := ini;
+        in go low
+  };
+
\ No newline at end of file diff --git a/Stdlib.Data.Range.html b/Stdlib.Data.Range.html new file mode 100644 index 00000000..83f416c6 --- /dev/null +++ b/Stdlib.Data.Range.html @@ -0,0 +1,10 @@ + +Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Range

Definitions

type Range NSource#

An inclusive range of naturals

Constructors

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

type StepRange NSource#

Constructors

| mkStepRange { + range : Range N; + step : N + }

to {N} {{Natural N}} (l h : N) : Range NSource#

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

step {N} (r : Range N) (s : N) : StepRange NSource#

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

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

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

\ No newline at end of file diff --git a/Stdlib.Data.Result-src.html b/Stdlib.Data.Result-src.html index 032c693b..56e6444b 100644 --- a/Stdlib.Data.Result-src.html +++ b/Stdlib.Data.Result-src.html @@ -8,6 +8,7 @@ import Stdlib.Trait.Ord open; import Stdlib.Trait.Functor open; +{-# specialize: true, inline: case #-} instance ordResultI {A B} {{Ord A}} {{Ord B}} : Ord (Result A B) := mkOrd@{ @@ -18,6 +19,7 @@ | (ok _) (error _) := GT }; +{-# specialize: true, inline: case #-} instance eqResultI {A B} {{Eq A}} {{Eq B}} : Eq (Result A B) := mkEq@{ @@ -27,14 +29,16 @@ | _ _ := false }; +{-# specialize: true, inline: case #-} instance functorResultI {err} : Functor (Result err) := mkFunctor@{ map := mapOk }; +{-# specialize: true, inline: true #-} instance monomorphicFunctorResultI {err res} : Monomorphic.Functor (Result err res) res := fromPolymorphicFunctor; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Data.Result.Base-src.html b/Stdlib.Data.Result.Base-src.html index 9417dbb7..a43ad67d 100644 --- a/Stdlib.Data.Result.Base-src.html +++ b/Stdlib.Data.Result.Base-src.html @@ -53,4 +53,4 @@ maybeToResult {E A} (defaultError : E) : Maybe A -> Result E A | nothing := error defaultError | (just x) := ok x; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Data.Result.Base.html b/Stdlib.Data.Result.Base.html index 775bcb49..db30e1d7 100644 --- a/Stdlib.Data.Result.Base.html +++ b/Stdlib.Data.Result.Base.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Data.Result.Base

Definitions

type Result E ASource#

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

Constructors

| error E
| ok A

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

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

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

Apply a function to the error value of a Result.

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

Apply a function to the ok value of a Result.

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

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

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

Return true if the value is ok, otherwise false.

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

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

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

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

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

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

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

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

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

Stdlib.Data.Result.Base

Definitions

type Result E ASource#

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

Constructors

| error E
| ok A

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

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

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

Apply a function to the error value of a Result.

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

Apply a function to the ok value of a Result.

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

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

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

Return true if the value is ok, otherwise false.

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

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

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

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

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

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

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

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

\ No newline at end of file diff --git a/Stdlib.Data.Result.html b/Stdlib.Data.Result.html index cacfe8f9..ff33f204 100644 --- a/Stdlib.Data.Result.html +++ b/Stdlib.Data.Result.html @@ -3,4 +3,4 @@ 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#

instance functorResultI {err} : Functor (Result err)Source#

instance -monomorphicFunctorResultI {err res} : Monomorphic.Functor (Result err res) resSource#

\ No newline at end of file +monomorphicFunctorResultI {err res} : Monomorphic.Functor (Result err res) resSource#

\ No newline at end of file diff --git a/Stdlib.Data.String-src.html b/Stdlib.Data.String-src.html index b48f9905..7aeea068 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; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Data.String.Base-src.html b/Stdlib.Data.String.Base-src.html index f7890153..4402d050 100644 --- a/Stdlib.Data.String.Base-src.html +++ b/Stdlib.Data.String.Base-src.html @@ -11,4 +11,4 @@ --- Joins a ;List; of ;String;s with "\n". unlines : List String -> String := intersperse "\n" >> concatStr; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Data.String.Base.html b/Stdlib.Data.String.Base.html index 18190a01..1bc893f2 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 cbe4b3cc..b3282ca6 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; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Data.String.Ord.html b/Stdlib.Data.String.Ord.html index 37ea1bc1..c7b9e9ff 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 2c50cbce..47cae106 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 febfb5bc..669e4132 100644 --- a/Stdlib.Data.Unit-src.html +++ b/Stdlib.Data.Unit-src.html @@ -22,10 +22,13 @@ instance showUnitI : Show Unit := mkShow λ {unit := "unit"}; +{-# specialize: true, inline: case #-} instance foldableUnitI : Foldable Unit Unit := mkFoldable@{ + {-# inline: true #-} rfor {B : Type} (f : B -> Unit -> B) (ini : B) (_ : Unit) : B := f ini unit; + {-# inline: true #-} for {B : Type} (f : B -> Unit -> B) (ini : B) (_ : Unit) : B := f ini unit }; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Data.Unit.html b/Stdlib.Data.Unit.html index dfea1ddb..62faafa3 100644 --- a/Stdlib.Data.Unit.html +++ b/Stdlib.Data.Unit.html @@ -3,4 +3,4 @@ eqUnitI : Eq UnitSource#

instance ordUnitI : Ord UnitSource#

instance showUnitI : Show UnitSource#

instance -foldableUnitI : Foldable Unit UnitSource#

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

\ No newline at end of file diff --git a/Stdlib.Debug.Fail-src.html b/Stdlib.Debug.Fail-src.html index 03223c45..ad54f7b2 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; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Debug.Fail.html b/Stdlib.Debug.Fail.html index 49675ac3..71832496 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 192330b9..0673b6dc 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; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Function.html b/Stdlib.Function.html index 61dcd594..d94b8bbe 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 9e0c9560..ef9a32b5 100644 --- a/Stdlib.Prelude-src.html +++ b/Stdlib.Prelude-src.html @@ -15,8 +15,9 @@ import Stdlib.Data.Pair open public; import Stdlib.Data.String open public; import Stdlib.Data.Result open public; +import Stdlib.Data.Range open public; import Stdlib.Function open public; import Stdlib.System.IO open public; import Stdlib.Trait open public; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Prelude.html b/Stdlib.Prelude.html index 547530a5..ed3693cc 100644 --- a/Stdlib.Prelude.html +++ b/Stdlib.Prelude.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Prelude

Description

This module reexports most of the standard library.

Definitions

import Stdlib.Data.Fixity open public

import Stdlib.Data.Bool open public

import Stdlib.Data.Byte open public

import Stdlib.Data.Unit open public

import Stdlib.Data.List open public

import Stdlib.Data.Maybe open public

import Stdlib.Data.Nat open public

import Stdlib.Data.Int open public

import Stdlib.Data.Field open public

import Stdlib.Data.Pair open public

import Stdlib.Data.String open public

import Stdlib.Data.Result open public

import Stdlib.Function open public

import Stdlib.System.IO open public

import Stdlib.Trait open public

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

Stdlib.Prelude

Description

This module reexports most of the standard library.

Definitions

import Stdlib.Data.Fixity open public

import Stdlib.Data.Bool open public

import Stdlib.Data.Byte open public

import Stdlib.Data.Unit open public

import Stdlib.Data.List open public

import Stdlib.Data.Maybe open public

import Stdlib.Data.Nat open public

import Stdlib.Data.Int open public

import Stdlib.Data.Field open public

import Stdlib.Data.Pair open public

import Stdlib.Data.String open public

import Stdlib.Data.Result open public

import Stdlib.Data.Range open public

import Stdlib.Function open public

import Stdlib.System.IO open public

import Stdlib.Trait open public

\ No newline at end of file diff --git a/Stdlib.System.IO-src.html b/Stdlib.System.IO-src.html index d77a49b0..a0bc427e 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); - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.System.IO.Base-src.html b/Stdlib.System.IO.Base-src.html index 41210270..e7169091 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; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.System.IO.Base.html b/Stdlib.System.IO.Base.html index c43993f2..261b077e 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 e536e39d..da4ec645 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"; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.System.IO.Bool.html b/Stdlib.System.IO.Bool.html index 4cca9452..542c1981 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 cd914a47..4ec97458 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"; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.System.IO.Int.html b/Stdlib.System.IO.Int.html index d8734701..52b4693a 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 40ad485b..5ae24c2e 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"; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.System.IO.Nat.html b/Stdlib.System.IO.Nat.html index bb20c809..3cb6ac44 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 862e141d..46f4920a 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"; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.System.IO.String.html b/Stdlib.System.IO.String.html index 940b041f..d854e046 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 b7ad161b..b44a3c26 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 ba18a7b1..922029fe 100644 --- a/Stdlib.Trait-src.html +++ b/Stdlib.Trait-src.html @@ -12,4 +12,4 @@ import Stdlib.Trait.Integral open public; import Stdlib.Trait.Numeric open public; import Stdlib.Trait.DivMod open public; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Trait.DivMod-src.html b/Stdlib.Trait.DivMod-src.html index d71bdde1..8243ba0f 100644 --- a/Stdlib.Trait.DivMod-src.html +++ b/Stdlib.Trait.DivMod-src.html @@ -11,4 +11,4 @@ }; open DivMod public; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Trait.DivMod.html b/Stdlib.Trait.DivMod.html index fde53fe3..575c7133 100644 --- a/Stdlib.Trait.DivMod.html +++ b/Stdlib.Trait.DivMod.html @@ -5,4 +5,4 @@ div : A -> A -> A; {-# isabelle-operator: {name: "mod", prec: 70, assoc: left} #-} mod : A -> A -> A - }

open DivMod public

\ No newline at end of file + }

open DivMod public

\ No newline at end of file diff --git a/Stdlib.Trait.Eq-src.html b/Stdlib.Trait.Eq-src.html index 6505be51..01195d34 100644 --- a/Stdlib.Trait.Eq-src.html +++ b/Stdlib.Trait.Eq-src.html @@ -15,6 +15,6 @@ == {A} {{Eq A}} : A -> A -> Bool := Eq.eq; --- Tests for inequality. -{-# inline: always, isabelle-operator: {name: "≠", prec: 50, assoc: none} #-} +{-# inline: always, isabelle-operator: {name: "\\<noteq>", prec: 50, assoc: none} #-} /= {A} {{Eq A}} (x y : A) : Bool := not (x == y); - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Trait.Eq.html b/Stdlib.Trait.Eq.html index 8363b18e..9e2b36fb 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.Foldable-src.html b/Stdlib.Trait.Foldable-src.html index 0f32ce2c..900e7442 100644 --- a/Stdlib.Trait.Foldable-src.html +++ b/Stdlib.Trait.Foldable-src.html @@ -3,4 +3,4 @@ import Stdlib.Trait.Foldable.Polymorphic as Polymorphic public; import Stdlib.Trait.Foldable.Monomorphic open public; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Trait.Foldable.Monomorphic-src.html b/Stdlib.Trait.Foldable.Monomorphic-src.html index 4ac87249..444d30ea 100644 --- a/Stdlib.Trait.Foldable.Monomorphic-src.html +++ b/Stdlib.Trait.Foldable.Monomorphic-src.html @@ -5,15 +5,14 @@ import Stdlib.Trait.Foldable.Polymorphic as Poly; --- A trait for combining elements into a single result, processing one element at a time. +{-# specialize: true #-} trait type Foldable (container elem : Type) := mkFoldable { syntax iterator for {init := 1; range := 1}; - {-# inline: 0 #-} for : {B : Type} -> (B -> elem -> B) -> B -> container -> B; syntax iterator rfor {init := 1; range := 1}; - {-# inline: 0 #-} rfor : {B : Type} -> (B -> elem -> B) -> B → container → B }; @@ -21,6 +20,7 @@ --- Make a monomorphic ;Foldable; instance from a polymorphic one. --- All polymorphic types that are an instance of ;Poly.Foldable; should use this function to create their monomorphic ;Foldable; instance. +{-# inline: case #-} fromPolymorphicFoldable {f : Type -> Type} {{foldable : Poly.Foldable f}} @@ -30,8 +30,9 @@ for := Poly.for; rfor := Poly.rfor }; - -foldl + +{-# inline: true #-} +foldl {container elem} {{Foldable container elem}} {B : Type} @@ -41,10 +42,11 @@ : B := for (acc := ini) (x in ls) {g acc x}; --- Combine the elements of the type using the provided function starting with the element in the right-most position. +{-# inline: 2 #-} foldr {container elem : Type} {{Foldable container elem}} {B : Type} (g : elem -> B -> B) : B -> container -> B := foldl (flip g); - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Trait.Foldable.Monomorphic.html b/Stdlib.Trait.Foldable.Monomorphic.html index 12ad7194..8f2ae81e 100644 --- a/Stdlib.Trait.Foldable.Monomorphic.html +++ b/Stdlib.Trait.Foldable.Monomorphic.html @@ -2,10 +2,8 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Foldable.Monomorphic

Definitions

trait type Foldable (container elem : Type)Source#

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

Constructors

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

open Foldable public

fromPolymorphicFoldable {f : Type -> Type} @@ -23,4 +21,4 @@ {{Foldable container elem}} {B : Type} (g : elem -> B -> B) - : B -> container -> BSource#

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

\ No newline at end of file + : B -> container -> BSource#

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

\ No newline at end of file diff --git a/Stdlib.Trait.Foldable.Polymorphic-src.html b/Stdlib.Trait.Foldable.Polymorphic-src.html index b8be6de2..9963f72a 100644 --- a/Stdlib.Trait.Foldable.Polymorphic-src.html +++ b/Stdlib.Trait.Foldable.Polymorphic-src.html @@ -8,17 +8,16 @@ type Foldable (f : Type -> Type) := mkFoldable { syntax iterator for {init := 1; range := 1}; - {-# inline: 0 #-} for : {A B : Type} -> (B -> A -> B) -> B -> f A -> B; syntax iterator rfor {init := 1; range := 1}; - {-# inline: 0 #-} rfor : {A B : Type} -> (B → A → B) -> B → f A → B }; open Foldable public; --- Combine the elements of the type using the provided function starting with the element in the left-most position. +{-# inline: true #-} foldl {f : Type -> Type} {{Foldable f}} @@ -29,6 +28,7 @@ : B := for (acc := ini) (x in ls) {g acc x}; --- Combine the elements of the type using the provided function starting with the element in the right-most position. +{-# inline: true #-} foldr {f : Type -> Type} {{Foldable f}} @@ -37,4 +37,4 @@ (ini : B) (ls : f A) : B := rfor (acc := ini) (x in ls) {g x acc}; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Trait.Foldable.Polymorphic.html b/Stdlib.Trait.Foldable.Polymorphic.html index c4fae861..f0b4e3ac 100644 --- a/Stdlib.Trait.Foldable.Polymorphic.html +++ b/Stdlib.Trait.Foldable.Polymorphic.html @@ -2,10 +2,8 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Foldable.Polymorphic

Definitions

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

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

Constructors

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

open Foldable public

foldl {f : Type -> Type} @@ -21,4 +19,4 @@ (g : A -> B -> B) (ini : B) (ls : f A) - : BSource#

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

\ No newline at end of file + : BSource#

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

\ No newline at end of file diff --git a/Stdlib.Trait.Foldable.html b/Stdlib.Trait.Foldable.html index 7341cea5..c667b78e 100644 --- a/Stdlib.Trait.Foldable.html +++ b/Stdlib.Trait.Foldable.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Foldable

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

Stdlib.Trait.Foldable

\ No newline at end of file diff --git a/Stdlib.Trait.FromNatural-src.html b/Stdlib.Trait.FromNatural-src.html index 3acb7511..925ade8a 100644 --- a/Stdlib.Trait.FromNatural-src.html +++ b/Stdlib.Trait.FromNatural-src.html @@ -2,4 +2,4 @@ 
module Stdlib.Trait.FromNatural;
 
 import Juvix.Builtin.V1.Trait.FromNatural open public;
-
\ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Trait.FromNatural.html b/Stdlib.Trait.FromNatural.html index 57e7ea10..006bc9a9 100644 --- a/Stdlib.Trait.FromNatural.html +++ b/Stdlib.Trait.FromNatural.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.FromNatural

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

Stdlib.Trait.FromNatural

\ No newline at end of file diff --git a/Stdlib.Trait.Functor-src.html b/Stdlib.Trait.Functor-src.html index 40b0e729..ae1c1133 100644 --- a/Stdlib.Trait.Functor-src.html +++ b/Stdlib.Trait.Functor-src.html @@ -4,4 +4,4 @@ import Stdlib.Trait.Functor.Polymorphic open public; import Stdlib.Trait.Functor.Monomorphic as Monomorphic public; import Stdlib.Trait.Functor.Monomorphic open using {fromPolymorphicFunctor} public; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Trait.Functor.Monomorphic-src.html b/Stdlib.Trait.Functor.Monomorphic-src.html index e4765756..f300fb79 100644 --- a/Stdlib.Trait.Functor.Monomorphic-src.html +++ b/Stdlib.Trait.Functor.Monomorphic-src.html @@ -5,32 +5,37 @@ import Stdlib.Data.Unit open; import Stdlib.Trait.Functor.Polymorphic as Poly; +{-# specialize: true #-} trait type Functor (container elem : Type) := mkFunctor { syntax iterator map {init := 0; range := 1}; + {-# specialize: [1] #-} map : (elem -> elem) -> container -> container }; open Functor public; - -fromPolymorphicFunctor + +{-# inline: case #-} +fromPolymorphicFunctor {f : Type -> Type} {{Poly.Functor f}} {elem} : Functor (f elem) elem := mkFunctor@{ map := Poly.map }; syntax operator <$> lapp; +{-# inline: true #-} <$> {container elem} {{Functor container elem}} : (elem -> elem) -> container -> container := map; syntax operator $> lapp; +{-# inline: true #-} $> {container elem : Type} {{Functor container elem}} (fa : container) (b : elem) : container := λ {_ := b} <$> fa; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Trait.Functor.Monomorphic.html b/Stdlib.Trait.Functor.Monomorphic.html index 1db9b9a5..857d3eb2 100644 --- a/Stdlib.Trait.Functor.Monomorphic.html +++ b/Stdlib.Trait.Functor.Monomorphic.html @@ -2,6 +2,7 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Functor.Monomorphic

Definitions

trait type Functor (container elem : Type)Source#

Constructors

| mkFunctor { syntax iterator map {init := 0; range := 1}; + {-# specialize: [1] #-} map : (elem -> elem) -> container -> container }

open Functor public

fromPolymorphicFunctor {f : Type -> Type} {{Poly.Functor f}} {elem} : Functor (f elem) elemSource#

<$> @@ -12,4 +13,4 @@ {{Functor container elem}} (fa : container) (b : elem) - : containerSource#

\ No newline at end of file + : containerSource#

\ No newline at end of file diff --git a/Stdlib.Trait.Functor.Polymorphic-src.html b/Stdlib.Trait.Functor.Polymorphic-src.html index e1a7518e..348f57c5 100644 --- a/Stdlib.Trait.Functor.Polymorphic-src.html +++ b/Stdlib.Trait.Functor.Polymorphic-src.html @@ -4,22 +4,27 @@ import Stdlib.Data.Fixity open; import Stdlib.Data.Unit open; +{-# specialize: true #-} trait type Functor (f : Type -> Type) := mkFunctor { syntax iterator map {init := 0; range := 1}; + {-# specialize: [1] #-} map : {A B : Type} -> (A -> B) -> f A -> f B }; open Functor public; syntax operator <$> lapp; +{-# inline: true #-} <$> {f : Type -> Type} {{Functor f}} {A B} : (A -> B) -> f A -> f B := map; syntax operator $> lapp; +{-# inline: true #-} $> {f : Type → Type} {A B : Type} {{Functor f}} (fa : f A) (b : B) : f B := λ {_ := b} <$> fa; - -void {f : Type → Type} {A : Type} {{Functor f}} (fa : f A) : f Unit := + +{-# inline: true #-} +void {f : Type → Type} {A : Type} {{Functor f}} (fa : f A) : f Unit := fa $> unit; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Trait.Functor.Polymorphic.html b/Stdlib.Trait.Functor.Polymorphic.html index f3f90196..e1efd50d 100644 --- a/Stdlib.Trait.Functor.Polymorphic.html +++ b/Stdlib.Trait.Functor.Polymorphic.html @@ -2,5 +2,6 @@ Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Functor.Polymorphic

Definitions

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

Constructors

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

open Functor public

<$> {f : Type -> Type} {{Functor f}} {A B} : (A -> B) -> f A -> f BSource#

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

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

\ No newline at end of file + }

open Functor public

<$> {f : Type -> Type} {{Functor f}} {A B} : (A -> B) -> f A -> f BSource#

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

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

\ No newline at end of file diff --git a/Stdlib.Trait.Functor.html b/Stdlib.Trait.Functor.html index bd9ab73b..b8bd4f32 100644 --- a/Stdlib.Trait.Functor.html +++ b/Stdlib.Trait.Functor.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait.Functor

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

Stdlib.Trait.Functor

\ No newline at end of file diff --git a/Stdlib.Trait.Integral-src.html b/Stdlib.Trait.Integral-src.html index 99f420b5..edcc3994 100644 --- a/Stdlib.Trait.Integral-src.html +++ b/Stdlib.Trait.Integral-src.html @@ -17,4 +17,4 @@ }; open Integral using {fromInt; -} public; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Trait.Integral.html b/Stdlib.Trait.Integral.html index f1f2866c..03b2b565 100644 --- a/Stdlib.Trait.Integral.html +++ b/Stdlib.Trait.Integral.html @@ -7,4 +7,4 @@ - : A -> A -> A; builtin from-int fromInt : Int -> A - }

open Integral using {fromInt; -} public

\ No newline at end of file + }

open Integral using {fromInt; -} public

\ No newline at end of file diff --git a/Stdlib.Trait.Natural-src.html b/Stdlib.Trait.Natural-src.html index e6b7f369..70ad9ab1 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;
-
\ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Trait.Natural.html b/Stdlib.Trait.Natural.html index 429851e5..879bcdac 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 f51e55c5..58945481 100644 --- a/Stdlib.Trait.Numeric-src.html +++ b/Stdlib.Trait.Numeric-src.html @@ -13,4 +13,4 @@ }; open Numeric using {/} public; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Trait.Numeric.html b/Stdlib.Trait.Numeric.html index cd2da468..3ac9b0de 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 467f052d..488d28ed 100644 --- a/Stdlib.Trait.Ord-src.html +++ b/Stdlib.Trait.Ord-src.html @@ -38,7 +38,7 @@ syntax operator <= comparison; --- Returns ;true; iff the first element is less than or equal to the second. -{-# inline: always, isabelle-operator: {name: "≤", prec: 50, assoc: none} #-} +{-# inline: always, isabelle-operator: {name: "\\<le>", prec: 50, assoc: none} #-} <= {A} {{Ord A}} (x y : A) : Bool := case Ord.cmp x y of | EQ := true @@ -64,7 +64,7 @@ syntax operator >= comparison; --- Returns ;true; iff the first element is greater than or equal to the second. -{-# inline: always, isabelle-operator: {name: "≥", prec: 50, assoc: none} #-} +{-# inline: always, isabelle-operator: {name: "\\<ge>", prec: 50, assoc: none} #-} >= {A} {{Ord A}} (x y : A) : Bool := y <= x; --- Returns the smaller element. @@ -74,4 +74,4 @@ --- Returns the larger element. {-# inline: always #-} max {A} {{Ord A}} (x y : A) : A := ite (x > y) x y; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Trait.Ord.html b/Stdlib.Trait.Ord.html index 2152893f..7dbe62f4 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 63f61a79..d9df66fd 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}}; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Trait.Partial.html b/Stdlib.Trait.Partial.html index b2f62cf0..4fb76a75 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 40a973df..ce00fcd0 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}; - \ No newline at end of file + \ No newline at end of file diff --git a/Stdlib.Trait.Show.html b/Stdlib.Trait.Show.html index f75e8768..087c9fd7 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 3943911f..b812ad8d 100644 --- a/Stdlib.Trait.html +++ b/Stdlib.Trait.html @@ -1,2 +1,2 @@ -Juvix Documentation
stdlib - 0.0.1

Stdlib.Trait

Definitions

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

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

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

import Stdlib.Trait.Functor open public

import Stdlib.Trait.Foldable open public

import Stdlib.Trait.Partial open public

import Stdlib.Trait.Natural open public

import Stdlib.Trait.FromNatural open public

import Stdlib.Trait.Integral open public

import Stdlib.Trait.Numeric open public

import Stdlib.Trait.DivMod open public

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

Stdlib.Trait

Definitions

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

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

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

import Stdlib.Trait.Functor open public

import Stdlib.Trait.Foldable open public

import Stdlib.Trait.Partial open public

import Stdlib.Trait.Natural open public

import Stdlib.Trait.FromNatural open public

import Stdlib.Trait.Integral open public

import Stdlib.Trait.Numeric open public

import Stdlib.Trait.DivMod open public

\ No newline at end of file diff --git a/index-src.html b/index-src.html index 15a7b96e..14cbb580 100644 --- a/index-src.html +++ b/index-src.html @@ -16,4 +16,4 @@ import Stdlib.Data.String.Ord; import Stdlib.Cairo.Poseidon; - \ No newline at end of file + \ No newline at end of file diff --git a/index.html b/index.html index 5f480a4c..165cc9e2 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