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')

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