Auto-format all files

.github/workflows/rzk.yml

@@ -26,3 +26,16 @@ jobs:
             src/1-foundations/1-type-theory/exercises/*.rzk.md
             src/1-foundations/2-homotopy-type-theory/*.rzk.md
             src/1-foundations/2-homotopy-type-theory/exercises/*.rzk.md
+
+  check-formatting:
+    runs-on: ubuntu-latest
+    name: Check Rzk formatting
+    steps:
+      - uses: actions/checkout@v3
+
+      - name: Check formatting
+        uses: rzk-lang/[email protected]
+        with:
+          rzk-version: v0.7.2
+          typecheck: false
+          check-formatting: true

src/1-foundations/1-type-theory/04-dependent-function-types.rzk.md

@@ -12,7 +12,7 @@ An example is the polymorphic identity function:
 
 ```rzk
 #define id
-  (A : U)
+  ( A : U)
   : A → A
   := \ x → x
 ```
@@ -22,7 +22,7 @@ that switches the order of the arguments of a (curried) two-argument function:
 
 ```rzk
 #define swap
-  (A B C : U)
-  : (A → B → C) → (B → A → C)
+  ( A B C : U)
+  : ( A → B → C) → (B → A → C)
   := \ f y x → f x y
 ```

src/1-foundations/1-type-theory/05-product-types.rzk.md

@@ -12,7 +12,7 @@ so we define product types here in terms of those.
 ```rzk
 #define prod (A B : U)
   : U
-  := Σ (_ : A), B
+  := Σ (_ : A) , B
 ```
 
 To construct a pair, we can now simply use tuple syntax for
@@ -22,36 +22,36 @@ To use a pair, we can use pattern matching or introduce projections:
 
 ```rzk
 #define pr₁
-  (A B : U)
+  ( A B : U)
   : prod A B → A
-  := \ (a, _b) → a
+  := \ (a , _b) → a
 
 #define pr₂
-  (A B : U)
+  ( A B : U)
   : prod A B → B
-  := \ (_a, b) → b
+  := \ (_a , b) → b
 ```
 
 The recursor for product types can be defined as follows:
 
 ```rzk
 #define prod-rec
-  (A B : U)
-  : (C : U) → (A → B → C) → prod A B → C
-  := \ C f (a, b) → f a b
+  ( A B : U)
+  : ( C : U) → (A → B → C) → prod A B → C
+  := \ C f (a , b) → f a b
 ```
 
 Then instead of defining functions such as pr1 and pr2 directly by a defining equation, we could
 define
 
 ```rzk
 #define pr₁-via-rec
-  (A B : U)
+  ( A B : U)
   : prod A B → A
   := prod-rec A B A (\ a _b → a)
 
 #define pr₂-via-rec
-  (A B : U)
+  ( A B : U)
   : prod A B → B
   := prod-rec A B B (\ _a b → b)
 ```
@@ -61,19 +61,19 @@ we have to generalize the recursor:
 
 ```rzk
 #define prod-ind
-  (A B : U)
-  : (C : prod A B → U) → ((x : A) → (y : B) → C (x, y)) → (x : prod A B) → C x
-  := \ C f (x, y) → f x y
+  ( A B : U)
+  : ( C : prod A B → U) → ((x : A) → (y : B) → C (x , y)) → (x : prod A B) → C x
+  := \ C f (x , y) → f x y
 ```
 
 For example, in this way we can prove the propositional uniqueness principle, which says that
 every element of `#!rzk A × B` is equal to a pair. Specifically, we can construct a function
 
 ```rzk
 #define prod-uniq
-  (A B : U)
-  : (x : prod A B) → (pr₁ A B x, pr₂ A B x) =_{prod A B} x
-  := \ (a, b) → refl_{(a, b)}
+  ( A B : U)
+  : ( x : prod A B) → (pr₁ A B x , pr₂ A B x) =_{prod A B} x
+  := \ (a , b) → refl_{(a , b)}
 ```
 
 ## Unit type
@@ -86,15 +86,15 @@ Still, following the book, here is the recursor for the unit type:
 
 ```rzk
 #define Unit-rec
-  : (C : U) → C → Unit → C
+  : ( C : U) → C → Unit → C
   := \ _C c _unit → c
 ```
 
 And, similarly, the induction principle for the unit type:
 
 ```rzk
 #define Unit-ind
-  : (C : Unit → U) → C unit → (x : Unit) → C x
+  : ( C : Unit → U) → C unit → (x : Unit) → C x
   := \ _C c unit → c
 ```
 
@@ -103,7 +103,7 @@ which asserts that its only inhabitant is `#!rzk unit`:
 
 ```rzk
 #define Unit-uniq
-  : (x : Unit) → x = unit
+  : ( x : Unit) → x = unit
   := Unit-ind (\ x → x = unit) refl_{unit}
 ```
 
@@ -113,6 +113,6 @@ allowing to use `#!rzk refl` immediately:
 
 ```rzk
 #define Unit-uniq'
-  : (x : Unit) → x = unit
+  : ( x : Unit) → x = unit
   := \ _ → refl
 ```

src/1-foundations/1-type-theory/06-dependent-pair-types.rzk.md

@@ -10,16 +10,16 @@ This is a literate Rzk file:
 
 ```rzk
 #def pr₁-Σ
-  (A : U)
-  (B : A -> U)
-  : (Σ (x : A), B x) -> A
-  := \p -> first p
+  ( A : U)
+  ( B : A → U)
+  : ( Σ ( x : A) , B x) → A
+  := \ p → first p
 
 #def pr₂-Σ
-  (A : U)
-  (B : A -> U)
-  : (p : Σ (x : A), B x) -> (B (first p))
-  := \p -> second p
+  ( A : U)
+  ( B : A → U)
+  : ( p : Σ (x : A) , B x) → (B (first p))
+  := \ p → second p
 ```
 Recursor for $\Sigma$-types. They are called like this:
 
@@ -29,18 +29,18 @@ $$
 
 ```rzk
 #def rec-Σ
-  (A : U)
-  (B : A -> U)
-  (C : U)
-  : (g : (x : A) -> B x -> C) -> (p : Σ (x : A), B x) -> C
-  := \ g (a, b) -> g a b
+  ( A : U)
+  ( B : A → U)
+  ( C : U)
+  : ( g : (x : A) → B x → C) → (p : Σ (x : A) , B x) → C
+  := \ g (a , b) → g a b
 ```
 
 ```rzk
 #def ind-Σ
-  (A : U)
-  (B : A -> U)
-  (C : (Σ (x : A), B x) -> U)
-  : (g : (x : A) -> (y : B x) -> C (x, y)) -> (p : Σ (x : A), B x) -> C p
-  := \ g (a, b) -> g a b
+  ( A : U)
+  ( B : A → U)
+  ( C : (Σ (x : A) , B x) → U)
+  : ( g : (x : A) → (y : B x) → C (x , y)) → (p : Σ (x : A) , B x) → C p
+  := \ g (a , b) → g a b
 ```

src/1-foundations/1-type-theory/12-identity-types.rzk.md

@@ -10,54 +10,54 @@ Induction on identity type is defined with built-in `idJ` operator:
 
 ```rzk
 #def path-ind
-  (A : U)
-  (C : (x : A) -> (y : A) -> (x = y) -> U)
-  (d : (x : A) -> C x x refl)
-  : (x : A) -> (y : A) -> (p : x = y) -> C x y p
-  := \ x y p -> idJ( A , x , C x , d x , y , p )
+  ( A : U)
+  ( C : (x : A) → (y : A) → (x = y) → U)
+  ( d : (x : A) → C x x refl)
+  : ( x : A) → (y : A) → (p : x = y) → C x y p
+  := \ x y p → idJ(A , x , C x , d x , y , p)
 ```
 
 Indiscernability of identicals:
 
 ```rzk
 #def indiscernability-of-identicals
-  (A : U)
-  (C : A → U)
-  : (x : A) → (y : A) → (p : x = y) → (C x) → (C y)
+  ( A : U)
+  ( C : A → U)
+  : ( x : A) → (y : A) → (p : x = y) → (C x) → (C y)
   := path-ind
     A
-    (\ x y p → ((C x) → (C y)))
-    (\ x → \ cx → cx)
+    ( \ x y p → ((C x) → (C y)))
+    ( \ x → \ cx → cx)
 ```
 
 Based path induction directly corresponds to the `idJ` operator:
 
 ```rzk
 #def based-path-ind
-  (A : U)
-  (a : A)   
-  (C : (x : A) → (a = x) → U)
-  (ca : C a refl)
-  : (x : A) → (p : a = x) → (C x p)
-  := \ x p → idJ( A , a , C , ca , x , p )
+  ( A : U)
+  ( a : A)   
+  ( C : (x : A) → (a = x) → U)
+  ( ca : C a refl)
+  : ( x : A) → (p : a = x) → (C x p)
+  := \ x p → idJ(A , a , C , ca , x , p)
 ```
 
 
 Based path induction can be defined with the (usual) path induction:
 
 ```rzk
 #def based-path-ind'
-  (A : U)
-  : (a : A) → 
-  (C : (x : A) → (a = x) → U) →
-  (ca : C a refl) →
-  (x : A) → 
-  (p : a = x) → 
-  (C x p)
+  ( A : U)
+  : ( a : A)
+  → ( C : (x : A) → (a = x) → U)
+  → ( ca : C a refl)
+  → ( x : A)
+  → ( p : a = x)
+  → ( C x p)
   := \ a C ca x p → 
   path-ind 
     A
-    (\ a' x' p' → (C' : ((x'' : A) → (a' = x'') → U)) → (C' a' refl) → (C' x' p'))
-    (\ a' → \ C' ca' → ca')
+    ( \ a' x' p' → (C' : ((x'' : A) → (a' = x'') → U)) → (C' a' refl) → (C' x' p'))
+    ( \ a' → \ C' ca' → ca')
     a x p C ca
 ```

src/1-foundations/1-type-theory/exercises/1.1-solution.rzk.md

@@ -43,9 +43,9 @@ This can be represented in rzk like so:
 
 ```rzk
 #define compose
-  (A B C : U)
-  (g : B → C)
-  (f : A → B)
+  ( A B C : U)
+  ( g : B → C)
+  ( f : A → B)
   : A → C
   := \ x → g (f x)
 ```
@@ -54,10 +54,10 @@ Associativity is automatic (by `refl`):
 
 ```rzk
 #define composition-associativity
-  (A B C D : U)
-  (f : A -> B)
-  (g : B -> C)
-  (h : C -> D)
+  ( A B C D : U)
+  ( f : A → B)
+  ( g : B → C)
+  ( h : C → D)
   : compose A C D h (compose A B C g f) = compose A B D (compose B C D h g) f
   := refl
 ```

src/1-foundations/1-type-theory/exercises/1.11-solution.rzk.md

@@ -22,8 +22,8 @@ The term `\ g → g a` has the required type.
 
 ```rzk
 #def triple-neg
-  (A : U)
-  : (((A → ⊥) → ⊥) → ⊥) → (A → ⊥)
+  ( A : U)
+  : ( ( ( A → ⊥) → ⊥) → ⊥) → (A → ⊥)
   := \ f a → f (\ g → g a)
 ```
 
@@ -32,7 +32,7 @@ it is possible to generalise the solution to an arbitrary type `B` instead of `
 
 ```rzk
 #def triple-neg'
-  (A B : U)
-  : (((A → B) → B) → B) → (A → B)
+  ( A B : U)
+  : ( ( ( A → B) → B) → B) → (A → B)
   := \ f a → f (\ g → g a)
 ```