Merge pull request #699 from stepchowfun/underscore

Let an obvious type be inferred
stepchowfun · Jan 25, 2025 · 2e81776 · 2e81776
2 parents b304e52 + 0a4a91e
commit 2e81776
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/proofs/tutorial/lesson2_dependent_types.v b/proofs/tutorial/lesson2_dependent_types.v
@@ -324,7 +324,7 @@ Fail Check
 *)
 
 Check
-  match Nat.even n as b return BoolToType b -> nat with
+  match Nat.even n as b return BoolToType b -> _ with
   | true => fun y => y + 1
   | false => fun y => length y
   end x.