From 0a4a91ea3fcefd574df31fdc993d549406531df8 Mon Sep 17 00:00:00 2001 From: Stephan Boyer Date: Sat, 25 Jan 2025 04:31:23 -0800 Subject: [PATCH] Let an obvious type be inferred --- proofs/tutorial/lesson2_dependent_types.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proofs/tutorial/lesson2_dependent_types.v b/proofs/tutorial/lesson2_dependent_types.v index dfbf4ee6..6cfa3fcd 100644 --- 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.