Fix typechecking for pragmas.juvix and add docs for default vals args.

docs/index.md

@@ -185,29 +185,29 @@ flowchart LR
     B -- VampIR --> C[PLONK or Halo2 circuit]
 ```
 
-``` shell
+```shell
 juvix compile -t vampir Hash.juvix
 ```
 
 The VampIR file can then be compiled to a PLONK circuit:
 
-``` shell
+```shell
 vamp-ir plonk setup -m 14 -o input.pp
 vamp-ir plonk compile -u input.pp -s Hash.pir -o c.plonk
 ```
 
 A zero-knowledge proof that `hash 1367` is equal to `3` can then be generated
 from the circuit:
 
-``` shell
+```shell
 vamp-ir plonk prove -u input.pp \
                     -c c.plonk \
                     -o proof.plonk -i Hash.json
 ```
 
 This proof can then be verified:
 
-``` shell
+```shell
 vamp-ir plonk verify -u input.pp -c c.plonk -p proof.plonk
 ```
 

docs/index/juvix.lock.yaml

@@ -2,48 +2,48 @@
 # Do not edit this file manually.
 
 dependencies:
-- git:
-    name: stdlib
-    ref: 8493ff47a0c2fad4542c8e75f5736060ae7da0a4
-    url: https://github.com/anoma/juvix-stdlib
-  dependencies: []
-- git:
-    name: taiga-simulator
-    ref: bcb9971b32aed93bdb1121182f41057d9625e0a9
-    url: https://github.com/anoma/taiga-simulator
-  dependencies:
   - git:
       name: stdlib
       ref: 8493ff47a0c2fad4542c8e75f5736060ae7da0a4
       url: https://github.com/anoma/juvix-stdlib
     dependencies: []
   - git:
-      name: test
-      ref: 3214a53b09a90fa77684a30d0fb2e14c202e99b5
-      url: https://github.com/anoma/juvix-test
+      name: taiga-simulator
+      ref: bcb9971b32aed93bdb1121182f41057d9625e0a9
+      url: https://github.com/anoma/taiga-simulator
     dependencies:
-    - git:
-        name: stdlib
-        ref: 8493ff47a0c2fad4542c8e75f5736060ae7da0a4
-        url: https://github.com/anoma/juvix-stdlib
-      dependencies: []
-  - git:
-      name: juvix-containers
-      ref: 7458d586a93caf9cc0ff678ef019c776c9f9b09f
-      url: https://github.com/anoma/juvix-containers
-    dependencies:
-    - git:
-        name: stdlib
-        ref: 8493ff47a0c2fad4542c8e75f5736060ae7da0a4
-        url: https://github.com/anoma/juvix-stdlib
-      dependencies: []
-    - git:
-        name: test
-        ref: 3214a53b09a90fa77684a30d0fb2e14c202e99b5
-        url: https://github.com/anoma/juvix-test
-      dependencies:
       - git:
           name: stdlib
           ref: 8493ff47a0c2fad4542c8e75f5736060ae7da0a4
           url: https://github.com/anoma/juvix-stdlib
         dependencies: []
+      - git:
+          name: test
+          ref: 3214a53b09a90fa77684a30d0fb2e14c202e99b5
+          url: https://github.com/anoma/juvix-test
+        dependencies:
+          - git:
+              name: stdlib
+              ref: 8493ff47a0c2fad4542c8e75f5736060ae7da0a4
+              url: https://github.com/anoma/juvix-stdlib
+            dependencies: []
+      - git:
+          name: juvix-containers
+          ref: 7458d586a93caf9cc0ff678ef019c776c9f9b09f
+          url: https://github.com/anoma/juvix-containers
+        dependencies:
+          - git:
+              name: stdlib
+              ref: 8493ff47a0c2fad4542c8e75f5736060ae7da0a4
+              url: https://github.com/anoma/juvix-stdlib
+            dependencies: []
+          - git:
+              name: test
+              ref: 3214a53b09a90fa77684a30d0fb2e14c202e99b5
+              url: https://github.com/anoma/juvix-test
+            dependencies:
+              - git:
+                  name: stdlib
+                  ref: 8493ff47a0c2fad4542c8e75f5736060ae7da0a4
+                  url: https://github.com/anoma/juvix-stdlib
+                dependencies: []

docs/reference/language/functions.juvix

@@ -80,3 +80,10 @@ module anonymous-functions;
     };
 --8<-- [end:anonymousFunctions]
 end;
+
+module default-values;
+  --8<-- [start:defaultValues]
+  import Stdlib.Prelude open;
+  f {x : Nat := 0}  {y : Nat := 1} :  Nat := x + y;
+  --8<-- [end:defaultValues]
+end;

docs/reference/language/functions.md

@@ -42,6 +42,48 @@ function's body to return `2 * n`.
 --8<------ "docs/reference/language/functions.juvix:multiplyByTwo"
 ```
 
+### Default Values
+
+We can assign default values to function arguments. This feature allows a
+function to operate without explicit argument values by using the provided
+defaults.
+
+To specify a default value for an argument, use the `:=` operator followed by
+the desired value. In the following example, `x` and `y` are given default
+values of `0` and `1`, respectively:
+
+
+```juvix
+--8<------ "docs/reference/language/functions.juvix:defaultValues"
+```
+
+
+When calling this function without providing values for `x` and `y`, such as
+`f`, the function will use the default values and return `1`.
+
+!!! note
+
+    Here are some key points to remember about using default argument values in
+    Juvix:
+
+    1. **No Referencing Previous Arguments**: Default values cannot refer to
+      previous arguments. Therefore, the following code would result in a scope
+      error:
+
+        ```juvix
+        f {n : Nat := 0} {m : Nat := n + 1} ....
+        ```
+
+    2. **Function-Specific Feature**: Only functions can have default values. Other
+      constructs or types do not support this feature.
+
+    3. **Left-Hand Side Limitation**: Only arguments on the left-hand side (LHS) of
+      the `:` can have default values. The following syntax is invalid:
+
+        ```juvix
+        f : {n : Nat := 0} := ...
+        ```
+
 ## Pattern Matching in Function Declarations
 
 A function may consist of one or more function clauses instead of a single

docs/reference/language/pragmas.juvix

@@ -51,8 +51,8 @@ module specialisations;
     | (x :: xs) := f x :: map f xs;
 --8<-- [end:pragma-specialise-arg]
 
-  axiom T : Type;
-  axiom T' : Type;
+  syntax alias T := Nat;
+  syntax alias T' := Nat;
 
 --8<-- [start:pragma-map-g]
   map_g : List T -> List T'
@@ -93,8 +93,8 @@ end;
 
 module Y;
 --8<-- [start:pragma-specialise-instance-false]
+-- instance -- TODO: revise this
 {-# specialize: false #-}
-instance
 naturalNatI : Natural Nat := <body>;
 --8<-- [end:pragma-specialise-instance-false]
 end;