fix: pattern matching on UInt

src/library/compiler/erase_irrelevant.cpp

@@ -210,6 +210,16 @@ class erase_irrelevant_fn {
                            binding_body(minor));
     }
 
+    expr elim_uint_cases(name const & uint_name, buffer<expr> & args) {
+        lean_assert(args.size() == 3);
+        expr major = visit(args[1]);
+        expr minor = visit_minor(args[2]);
+        lean_assert(is_lambda(minor));
+        return
+          ::lean::mk_let(next_name(), mk_enf_object_type(), mk_app(mk_const(name(uint_name, "toNat")), major),
+                         binding_body(minor));
+    }
+
     expr decidable_to_bool_cases(buffer<expr> const & args) {
         lean_assert(args.size() == 5);
         expr const & major  = args[2];
@@ -235,6 +245,8 @@ class erase_irrelevant_fn {
             return elim_int_cases(args);
         } else if (I_name == get_array_name()) {
             return elim_array_cases(args);
+        } else if (I_name == get_uint8_name() || I_name == get_uint16_name() || I_name == get_uint32_name() || I_name == get_uint64_name() || I_name == get_usize_name()) {
+          return elim_uint_cases(I_name, args);
         } else if (I_name == get_decidable_name()) {
             return decidable_to_bool_cases(args);
         } else {

tests/lean/uintMatch.lean

@@ -0,0 +1,15 @@
+def f : UInt8 → Bool
+ | 5 => true
+ | _ => false
+
+#eval f 8
+#eval f 5
+
+def g : UInt32 → String
+ | 5    => "hello"
+ | 1555 => "world"
+ | _    => "bla"
+
+#eval g 5
+#eval g 1555
+#eval g 555

tests/lean/uintMatch.lean.expected.out

@@ -0,0 +1,5 @@
+false
+true
+"hello"
+"world"
+"bla"