Skip to content

Commit

Permalink
Fix: use extract-module-statements
Browse files Browse the repository at this point in the history
  • Loading branch information
jonaprieto committed Apr 19, 2024
1 parent 7a57cb8 commit 0a82cc2
Show file tree
Hide file tree
Showing 7 changed files with 82 additions and 82 deletions.
2 changes: 1 addition & 1 deletion docs/reference/language/builtins.juvix.md
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ builtin nat-plus

## Builtin axiom definitions

```juvix
```juvix extract-module-statements
module example-print-nat;
builtin IO
Expand Down
6 changes: 3 additions & 3 deletions docs/reference/language/datatypes.juvix.md
Original file line number Diff line number Diff line change
Expand Up @@ -109,7 +109,7 @@ the type of the data type being declared.

For example, the `Nat` type can be declared as follows:

```juvix
```juvix extract-module-statements
module Nat-ADT;
type Nat :=
| Z
Expand All @@ -120,7 +120,7 @@ end;
Another example is the `List` type, which is polymorphic in the type of its
elements.

```juvix
```juvix extract-module-statements
module List-ADT;
type List A :=
| Nil
Expand All @@ -145,7 +145,7 @@ the type of its list elements.

The following function determines whether an element is in a list or not.

```juvix
```juvix extract-module-statements 1
module membership;
import Stdlib.Data.Bool open using {Bool; false; ||};
Expand Down
6 changes: 3 additions & 3 deletions docs/reference/language/fixity.juvix.md
Original file line number Diff line number Diff line change
Expand Up @@ -100,7 +100,7 @@ The `or` operator will inherit the fixity of the `||` operator by default.
import reference.language.aliases open;
```

```juvix
```juvix extract-module-statements
module fixityInherit;
syntax alias or := ||;
newor (a b c : Bool) : Bool := (a or b) or c;
Expand All @@ -110,7 +110,7 @@ end;
However, if you want to override this behavior, you can declare the alias with
`none` as its fixity. Make sure to import `Stdlib.Data.Fixity`.

```juvix
```juvix extract-module-statements
module fixityNone;
import Stdlib.Data.Fixity open;
syntax operator or none;
Expand All @@ -124,7 +124,7 @@ end;
Here are some examples of common fixity declarations for operators in Juvix's
standard library.

```juvix
```juvix extract-module-statements
module examples-from-stdlib;
syntax fixity rapp := binary {assoc := right};
syntax fixity lapp := binary {assoc := left; same := rapp};
Expand Down
16 changes: 8 additions & 8 deletions docs/reference/language/functions.juvix.md
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ For example, consider the function `multiplyByTwo` which takes a `Nat` (natural
number) and returns a `Nat`. The argument is named `n` and is used in the
function's body to return `2 * n`.

```juvix
```juvix extract-module-statements 1
module example-multiply-by-two;
import Stdlib.Data.Nat open using {Nat; *};
multiplyByTwo (n : Nat) : Nat := 2 * n;
Expand All @@ -60,7 +60,7 @@ the desired value. In the following example, `x` and `y` are given default
values of `0` and `1`, respectively:


```juvix
```juvix extract-module-statements 1
module default-values;
import Stdlib.Prelude open;
f {x : Nat := 0} {y : Nat := 1} : Nat := x + y;
Expand Down Expand Up @@ -112,7 +112,7 @@ matches.

For instance, consider the following function with two clauses:

```juvix
```juvix extract-module-statements 1
module example-negate-boolean;
import Stdlib.Data.Bool open;
Expand All @@ -139,7 +139,7 @@ of two arguments is as follows and can be extended to more arguments.
Initial function arguments that match variables or wildcards in all clauses can
be moved to the left of the colon in the function definition. For example,

```juvix
```juvix extract-module-statements 1
module move-to-left;
import Stdlib.Data.Nat open;

Expand All @@ -151,7 +151,7 @@ of two arguments is as follows and can be extended to more arguments.

is equivalent to

```juvix
```juvix extract-module-statements 1
module example-add;
import Stdlib.Data.Nat open;
add : Nat -> Nat -> Nat
Expand All @@ -162,7 +162,7 @@ of two arguments is as follows and can be extended to more arguments.

If there is only one clause without any patterns, the pipe `|` must be omitted as we see earlier.

```juvix
```juvix extract-module-statements 1
module short-definitons;
import Stdlib.Data.Nat open;
multiplyByTwo (n : Nat) : Nat := n;
Expand All @@ -175,7 +175,7 @@ Functions in Juvix can depend on each other recursively. In the following
example, a function checks if a number is `even` by calling another function
that verifies if the number is `odd`.

```juvix
```juvix extract-module-statements 3
module mutually-recursive;
import Stdlib.Data.Nat open;
import Stdlib.Data.Bool open;
Expand Down Expand Up @@ -213,7 +213,7 @@ alternative `λ` to denote an anonymous function.
An anonymous function lists all clauses of a function without naming it. Any
function declaration can be converted to use anonymous functions:

```juvix
```juvix extract-module-statements 1
module anonymous-functions;
import Stdlib.Prelude open;
Expand Down
4 changes: 2 additions & 2 deletions docs/reference/language/pragmas.juvix.md
Original file line number Diff line number Diff line change
Expand Up @@ -231,7 +231,7 @@ symbolizes a non-negative number.
axiom <body> : Natural Nat;
```

```juvix
```juvix extract-module-statements
module pragma-specialise-instance;
{-# specialize: true #-}
instance
Expand All @@ -243,7 +243,7 @@ symbolizes a non-negative number.

Declaring

```juvix
```juvix extract-module-statements
module pragma-specialise-instance-false;
{-# specialize: false #-}
naturalNatI : Natural Nat := <body>;
Expand Down
2 changes: 1 addition & 1 deletion docs/reference/language/traits.juvix.md
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,7 @@ Using the `Show` trait defined above, we can define a function `showNat` that
takes a `Nat` and returns a `String`. One possible implementation is the
following:

```juvix
```juvix extract-module-statements
module usage-example;
type Nat :=
| Z
Expand Down
Loading

0 comments on commit 0a82cc2

Please sign in to comment.