New Iterator/Fixity record syntax

Stdlib/Data/Fixity.juvix

@@ -1,21 +1,21 @@
 module Stdlib.Data.Fixity;
 
-syntax fixity rapp {arity: binary, assoc: right};
-syntax fixity lapp {arity: binary, assoc: left, same: rapp};
-syntax fixity seq {arity: binary, assoc: left, above: [lapp]};
+syntax fixity rapp := binary {assoc := right};
+syntax fixity lapp := binary {assoc := left; same := rapp};
+syntax fixity seq := binary {assoc := left; above := [lapp]};
 
-syntax fixity functor {arity: binary, assoc: right};
+syntax fixity functor := binary {assoc := right};
 
-syntax fixity logical {arity: binary, assoc: right, above: [seq]};
-syntax fixity comparison {arity: binary, assoc: none, above: [logical]};
+syntax fixity logical := binary {assoc := right; above := [seq]};
+syntax fixity comparison := binary {assoc := none; above := [logical]};
 
-syntax fixity pair {arity: binary, assoc: right};
-syntax fixity cons {arity: binary, assoc: right, above: [pair]};
+syntax fixity pair := binary {assoc := right};
+syntax fixity cons := binary {assoc := right; above := [pair]};
 
-syntax fixity step {arity: binary, assoc: right};
-syntax fixity range {arity: binary, assoc: right, above: [step]};
+syntax fixity step := binary {assoc := right};
+syntax fixity range := binary {assoc := right; above := [step]};
 
-syntax fixity additive {arity: binary, assoc: left, above: [comparison, range, cons]};
-syntax fixity multiplicative {arity: binary, assoc: left, above: [additive]};
+syntax fixity additive := binary {assoc := left; above := [comparison; range; cons]};
+syntax fixity multiplicative := binary {assoc := left; above := [additive]};
 
-syntax fixity composition {arity: binary, assoc: right, above: [multiplicative]};
+syntax fixity composition := binary {assoc := right; above := [multiplicative]};

Stdlib/Data/Int/Range.juvix

@@ -14,7 +14,7 @@ type Range :=
     step : Int
   };
 
-syntax iterator for {init: 1, range: 1};
+syntax iterator for {init := 1; range := 1};
 
 {-# specialize: [1, 3] #-}
 for {A} (f : A → Int → A) (a : A) : Range → A

Stdlib/Data/List/Base.juvix

@@ -32,7 +32,7 @@ foldr {A B} (f : A → B → B) (z : B) : List A → B
   | nil := z
   | (h :: hs) := f h (foldr f z hs);
 
-syntax iterator rfor {init: 1, range: 1};
+syntax iterator rfor {init := 1; range := 1};
 
 {-# specialize: [1] #-}
 rfor {A B} (f : B → A → B) (acc : B) : List A → B
@@ -45,20 +45,20 @@ foldl {A B} (f : B → A → B) (z : B) : List A → B
   | nil := z
   | (h :: hs) := foldl f (f z h) hs;
 
-syntax iterator for {init: 1, range: 1};
+syntax iterator for {init := 1; range := 1};
 
 {-# inline: 0 #-}
 for : {A B : Type} → (B → A → B) → B → List A → B := foldl;
 
-syntax iterator map {init: 0, range: 1};
+syntax iterator map {init := 0; range := 1};
 
 --- 𝒪(𝓃). Maps a function over each element of a ;List;.
 {-# specialize: [1] #-}
 map {A B} (f : A → B) : List A → List B
   | nil := nil
   | (h :: hs) := f h :: map f hs;
 
-syntax iterator filter {init: 0, range: 1};
+syntax iterator filter {init := 0; range := 1};
 
 --- 𝒪(𝓃). Filters a ;List; according to a given predicate, i.e.,
 --- keeps the elements for which the given predicate returns ;true;.
@@ -146,15 +146,15 @@ tail {A} : List A → List A
   | (_ :: xs) := xs
   | nil := nil;
 
-syntax iterator any {init: 0, range: 1};
+syntax iterator any {init := 0; range := 1};
 
 --- 𝒪(𝓃). Returns ;true; if at least one element of the ;List; satisfies the predicate.
 {-# specialize: [1] #-}
 any {A} (f : A → Bool) : List A → Bool
   | nil := false
   | (x :: xs) := if (f x) true (any f xs);
 
-syntax iterator all {init: 0, range: 1};
+syntax iterator all {init := 0; range := 1};
 
 --- 𝒪(𝓃). Returns ;true; if all elements of the ;List; satisfy the predicate.
 {-# specialize: [1] #-}
@@ -220,7 +220,7 @@ catMaybes {A} : List (Maybe A) -> List A
   | (just h :: hs) := h :: catMaybes hs
   | (nothing :: hs) := catMaybes hs;
 
-syntax iterator concatMap {init: 0, range: 1};
+syntax iterator concatMap {init := 0; range := 1};
 
 --- Applies a function to every item on a ;List; and concatenates the result.
 --- 𝒪(𝓃), where 𝓃 is the number of items in the resulting list.

Stdlib/Data/Nat/Range.juvix

@@ -14,7 +14,7 @@ type Range :=
     step : Nat
   };
 
-syntax iterator for {init: 1, range: 1};
+syntax iterator for {init := 1; range := 1};
 
 {-# specialize: [1, 3] #-}
 for {A} (f : A → Nat → A) (a : A) : Range → A