Example of a Juvix program!

      Stdlib.Prelude> --example of a comment
      Stdlib.Prelude> 3 + 4
      7
      Stdlib.Prelude> 1 + 3 * 7
      22
      Stdlib.Prelude> div 35 4
      8
      Stdlib.Prelude> mod 35 4
      3
      Stdlib.Prelude> let x := 3 in x
      3
      Stdlib.Prelude> infixl 6 _+_;
      0
    

      module {- coment -} Demo.Example.Tutorial {-comment-} ;
-- {-- Inline comments are also supported. -}
-- -- Inline comments are also supported. --
--- Judoc comment.
-- {name1; name2}
-- {name1; name2;};
infix  {--- hhh --} 4  {--- hhh --} _≤_  {--- hhh --};
infixl 6 _+_;
infixr 7 op;
open import Stdlib.Prelude; import Stdlib.Data.Nat.Ord;
open import Stdlib.Data.Ord public; open import Stdlib.Data.Ord XXX public;
open import Stdlib.Data.Ord public --asdf;
open import Stdlib.Data.Ord public {--asdf--};
open import Stdlib.Map using {name1; name2 };
open import Stdlib.Map using {name1; 
-- comment
name2;
{- final comment here -}
};
open M;
open N public;
open import Stdlib.Map using {name1; name2} hiding {name3; name4} public;
open import Stdlib.Map hiding {name3; name4};

open import {--- hhh --} Stdlib.Data.Ord;
open import Stdlib.Data.Product 
-- comment in between 
  using 
  -- comment in between 
  {name1; name2}
  -- comment in the middle
  ;

module AA; 
 -- cmoment
end;

      module Format;

      open import Stdlib.Prelude hiding {,};
      open import Stdlib.Data.Nat.Ord;
      
      terminating
      go : Nat → Nat → Nat;
      go n s :=
        if
          (s < n)
          (go (sub n 1) s)
          (go n (sub s n) + go (sub n 1) s);
      
      module M;
        infixr 4 ,;
        axiom , : String → String → String;
      end;
      
      -- qualified commas
      t4 : String;
      t4 := "a" M., "b" M., "c" M., "d";
      
      open M;
      
      -- mix qualified and unqualified commas
      t5 : String;
      t5 := "a" M., "b" M., "c", "d";
      
      -- comma chain fits in a line
      t2 : String;
      t2 := "a", "b", "c", "d";
      
      -- comma chain does not fit in a line
      t3 : String;
      t3 :=
        "a"
          , "b"
          , "c"
          , "d"
          , "e"
          , "f"
          , "g"
          , "h"
          , "i"
          , "j"
          , "k"
          , "1234";
      
      infixl 7 +l7;
      axiom +l7 : String → String → String;
      
      infixr 3 +r3;
      axiom +r3 : String → String → String;
      
      infixl 1 +l1;
      axiom +l1 : String → String → String;
      
      infixl 6 +l6;
      axiom +l6 : String → String → String;
      
      infixr 6 +r6;
      axiom +r6 : String → String → String;
      
      -- nesting of chains
      t : String;
      t :=
        "Hellooooooooo"
          +l1 "Hellooooooooo"
          +l1 "Hellooooooooo"
              +l6 "Hellooooooooo"
              +l6 ("Hellooooooooo"
                +r6 "Hellooooooooo"
                +r6 "Hellooooooooo")
              +l6 "Hellooooooooo"
              +l6 "Hellooooooooo"
                +l7 "Hellooooooooo"
                +l7 "Hellooooooooo"
                +l7 "Hellooooooooo"
            , "hi"
            , "hi";
      
      -- function with single wildcard parameter
      g : (_ : Type) -> Nat;
      g _ := 1;
      
      -- grouping of type arguments
      exampleFunction1 :
        {A : Type}
          -> List A
          -> List A
          -> List A
          -> List A
          -> List A
          -> List A
          -> List A
          -> Nat;
      exampleFunction1 _ _ _ _ _ _ _ := 1;
      
      -- 200 in the body is idented with respect to the start of the chain
      -- (at {A : Type})
      exampleFunction2 :
        {A : Type}
          -> List A
          -> List A
          -> List A
          -> List A
          -> List A
          -> List A
          -> List A
          -> Nat :=
          200
            + 100
            + 100
            + 100
            + 100
            + 100
            + 100
            + 100
            + 100
            + 100
            + 100;
      
      module Patterns;
        infixr 4 ,;
        type Pair :=
          | , : String → String → String;
      
        -- Commas in patterns
        f : _;
        f (a, b, c, d) := a;
      end;
      -- Comment at the end of a module