Auto-format all files

.github/workflows/format.yml

@@ -20,3 +20,10 @@ jobs:
         with:
           dry: true
           prettier_options: --check **/*.{md,json,yaml,yml}
+
+      - name: Rzk formatter
+        uses: rzk-lang/[email protected]
+        with:
+          rzk-version: v0.7.2
+          typecheck: false
+          check-formatting: true

.vscode/settings.json

@@ -15,7 +15,7 @@
   "editor.inlineSuggest.enabled": true,
   "editor.acceptSuggestionOnEnter": "off",
   "editor.snippetSuggestions": "top",
-  "editor.wordBasedSuggestions": false,
+  "editor.wordBasedSuggestions": "off",
   "javascript.suggest.names": false,
 
   // Autoformatting and file type specific settings
@@ -61,5 +61,6 @@
     "editor.autoClosingBrackets": "never",
     "editor.detectIndentation": false,
     "editor.insertSpaces": true
-  }
+  },
+  "rzk.format.enable": true
 }

src/hott/00-common.rzk.md

@@ -90,20 +90,20 @@ The following demonstrates the syntax for constructing terms in Sigma types:
 ```rzk
 #def Map
   : U
-  := Σ ((A',A) : product U U) , (A' → A)
+  := Σ ((A' , A) : product U U) , (A' → A)
 
 #def the-map-Map
-  ( ((A',A),α) : Map)
+  ( ( ( A' , A) , α) : Map)
   : A' → A
   := α
 
 #def the-domain-Map
-  ( ((A',_),_) : Map)
+  ( ( ( A' , _) , _) : Map)
   : U
   := A'
 
 #def the-codomain-Map
-  ( ((_,A),_) : Map)
+  ( ( ( _ , A) , _) : Map)
   : U
   := A
 ```