Merge pull request #80 from rzk-lang/release-v0.6.1

Release v0.6.1

Author: fizruk

CHANGELOG.md

@@ -4,6 +4,23 @@ All notable changes to the "rzk-1-experimental-highlighting" extension will be d
 
 Check [Keep a Changelog](http://keepachangelog.com/) for recommendations on how to structure this file.
 
+## v0.6.1 - 2026-07-25
+
+This release updates the grammar to match `rzk` v0.11.1, which adds higher
+inductive types. The minimum supported `rzk` version is unchanged (v0.11.0);
+an extension-managed `rzk` picks up v0.11.1 on its own, since it always
+updates to the latest release the extension supports.
+
+- Highlight the re-ascription clauses `eliminate with` and `compute with`,
+  which replace the `eliminator` clause of `rzk` v0.11.0. Both are matched as
+  two-word sequences, as `let mod` already was, because `compute` on its own
+  is a plausible identifier and only the pair is a keyword.
+- The `into` motive of a modal `let mod` (new in `rzk` v0.11.1) needs no
+  grammar change: `into` was already a keyword for `match`.
+- Cover the new syntax in the tests: the circle with a path constructor and
+  both re-ascription clauses, taken from the `rzk` documentation and checked
+  against `rzk` v0.11.1, is added to the snapshot fixtures.
+
 ## v0.6.0 - 2026-07-21
 
 This release accompanies `rzk` v0.11.0 and pins the extension to it: the

package.json

@@ -3,7 +3,7 @@
   "displayName": "Rzk",
   "description": "Interactive theorem proving support in VS Code for Rzk, a proof assistant for synthetic ∞-categories",
   "icon": "images/icon.png",
-  "version": "0.6.0",
+  "version": "0.6.1",
   "repository": "https://github.com/rzk-lang/vscode-rzk",
   "publisher": "NikolaiKudasovfizruk",
   "main": "./out/extension.js",

syntaxes/rzk.tmLanguage.json

@@ -138,7 +138,11 @@
         },
         {
           "name": "keyword.control.rzk",
-          "match": "(?<=^|[.\\\\;,#\"\\]\\[)(}{><|\\s])(match|into|eliminator)(?=$|[.\\\\;,#\"\\]\\[)(}{><|\\s])"
+          "match": "(?<=^|[.\\\\;,#\"\\]\\[)(}{><|\\s])(match|into)(?=$|[.\\\\;,#\"\\]\\[)(}{><|\\s])"
+        },
+        {
+          "name": "keyword.control.rzk",
+          "match": "(?<=^|[.\\\\;,#\"\\]\\[)(}{><|\\s])(eliminate|compute)\\s+(with)(?=$|[.\\\\;,#\"\\]\\[)(}{><|\\s])"
         },
         {
           "name": "keyword.control.as.rzk",

syntaxes/rzk.tmLanguage.yml

@@ -70,7 +70,12 @@ repository:
       - name: support.function.rzk
         match: (?<=^|[.\\;,#"\]\[)(}{><|\s])(recOR|recBOT|idJ|refl|first|second|π₁|π₂|unit|sup|inf|invᵒᵖ|uninvᵒᵖ|flipᵒᵖ|unflipᵒᵖ|inv_op|uninv_op|flip_op|unflip_op)((?=$|[.\\;,#"\]\[)(}{><|\s])|(?=_{))
       - name: keyword.control.rzk
-        match: (?<=^|[.\\;,#"\]\[)(}{><|\s])(match|into|eliminator)(?=$|[.\\;,#"\]\[)(}{><|\s])
+        match: (?<=^|[.\\;,#"\]\[)(}{><|\s])(match|into)(?=$|[.\\;,#"\]\[)(}{><|\s])
+      # The re-ascription clauses of a #data body. Matched as two-word
+      # sequences, as `let mod` is below: `compute` on its own is a plausible
+      # identifier, and only the pair is a keyword.
+      - name: keyword.control.rzk
+        match: (?<=^|[.\\;,#"\]\[)(}{><|\s])(eliminate|compute)\s+(with)(?=$|[.\\;,#"\]\[)(}{><|\s])
       - name: keyword.control.as.rzk
         match: (?<=^|[.\\;,#"\]\[)(}{><|\s])as(?=$|[.\\;,#"\]\[)(}{><|\s])
       - name: keyword.control.rzk

tests/colorize/inductive.rzk

@@ -19,10 +19,17 @@ match
 into
 -- <-- keyword.control.rzk
 
--- the eliminator re-ascription clause of a #data body
-eliminator
+-- the re-ascription clauses of a #data body (rzk v0.11.1)
+eliminate with
 -- <-- keyword.control.rzk
 
+compute with
+-- <-- keyword.control.rzk
+
+-- neither word is a keyword on its own
+compute
+-- <-- source.rzk
+
 -- ASCII lattice operations are builtin functions
 sup
 -- <-- support.function.rzk

tests/fixtures/inductive.rzk

@@ -32,3 +32,32 @@
 
 #define join-unicode (a b : 𝕀) : 𝕀
   := a ⊔ (a ⊓ b)
+
+#define transport
+  ( A : U) (C : A → U) (x y : A) (p : x =_{A} y) (u : C x)
+  : C y
+  := idJ (A , x , \ y' _ → C x → C y' , \ v → v , y , p) u
+
+#define ap
+  ( A B : U) (f : A → B) (x y : A) (p : x =_{A} y)
+  : f x =_{B} f y
+  := idJ (A , x , \ y' _ → f x =_{B} f y' , refl , y , p)
+
+#data circle
+  :=
+    pt
+  | turn : pt =_{circle} pt
+  eliminate with ind-circle
+    : ( C : circle → U)
+    → ( b : C pt)
+    → ( ℓ : transport circle C pt pt turn b = b)
+    → ( x : circle)
+    → C x
+  compute with compute-rec-circle-turn
+    : ( C : U)
+    → ( b : C)
+    → ( ℓ : b = b)
+    → ap circle C (rec-circle C b ℓ) pt pt turn = ℓ
+
+#define circle-id (x : circle) : circle
+  := match x (pt ⇒ pt | turn ⇒ turn)