From cd5542fc82edee11181a43e3a342a2567c929e7e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 14:53:12 +0200
Subject: Regenerate the tests

---
 tests/lean/Matches.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'tests/lean/Matches.lean')

diff --git a/tests/lean/Matches.lean b/tests/lean/Matches.lean
index 3e3a558b..34f899b1 100644
--- a/tests/lean/Matches.lean
+++ b/tests/lean/Matches.lean
@@ -9,8 +9,8 @@ namespace matches
    Source: 'tests/src/matches.rs', lines 4:0-4:27 -/
 def match_u32 (x : U32) : Result U32 :=
   match x with
-  | 0#u32 => Result.ok 0#u32
-  | 1#u32 => Result.ok 1#u32
-  | _ => Result.ok 2#u32
+  | 0u32 => Result.ok 0u32
+  | 1u32 => Result.ok 1u32
+  | _ => Result.ok 2u32
 
 end matches
-- 
cgit v1.2.3


From d85d160ae9736f50d9c043b411c5a831f1fbb964 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 18:20:35 +0200
Subject: Revert "Regenerate the tests"

This reverts commit cd5542fc82edee11181a43e3a342a2567c929e7e.
---
 tests/lean/Matches.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'tests/lean/Matches.lean')

diff --git a/tests/lean/Matches.lean b/tests/lean/Matches.lean
index 34f899b1..3e3a558b 100644
--- a/tests/lean/Matches.lean
+++ b/tests/lean/Matches.lean
@@ -9,8 +9,8 @@ namespace matches
    Source: 'tests/src/matches.rs', lines 4:0-4:27 -/
 def match_u32 (x : U32) : Result U32 :=
   match x with
-  | 0u32 => Result.ok 0u32
-  | 1u32 => Result.ok 1u32
-  | _ => Result.ok 2u32
+  | 0#u32 => Result.ok 0#u32
+  | 1#u32 => Result.ok 1#u32
+  | _ => Result.ok 2#u32
 
 end matches
-- 
cgit v1.2.3


From 19abb19134efe0b16409f955b13af36262f231a8 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 18:40:27 +0200
Subject: Update the code extraction and regenerate the tests

---
 tests/lean/Matches.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tests/lean/Matches.lean')

diff --git a/tests/lean/Matches.lean b/tests/lean/Matches.lean
index 3e3a558b..9233841b 100644
--- a/tests/lean/Matches.lean
+++ b/tests/lean/Matches.lean
@@ -9,8 +9,8 @@ namespace matches
    Source: 'tests/src/matches.rs', lines 4:0-4:27 -/
 def match_u32 (x : U32) : Result U32 :=
   match x with
-  | 0#u32 => Result.ok 0#u32
-  | 1#u32 => Result.ok 1#u32
+  | 0#scalar => Result.ok 0#u32
+  | 1#scalar => Result.ok 1#u32
   | _ => Result.ok 2#u32
 
 end matches
-- 
cgit v1.2.3