From f8c5face564399f3dc57030599719b07a0a8e089 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 2 Nov 2019 12:12:27 -0700 Subject: [PATCH] chore: update --- tests/elabissues/issues1.lean | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/tests/elabissues/issues1.lean b/tests/elabissues/issues1.lean index a8e8cce4eb..542f3b5468 100644 --- a/tests/elabissues/issues1.lean +++ b/tests/elabissues/issues1.lean @@ -5,14 +5,7 @@ f [1, 2, 3] -- Works def ex2 : Bool := let xs := [1, 2, 3]; -/- The following application fails. - In the Lean3 elaborator, the `;` after `have` and `let` expressions is a "check-point". - The elaborator will resolve type class instances and force pending numeral types to `Nat` if they - have not been assigned yet. - So, `xs` will have type `List Nat`. - Solution: remove "check-point" from `let`, but keep the one on `have`. We use `have` expressions - when proving, and it is nice to make sure the proposition does not have meta-variables before continuing. -/ -f xs +f xs -- Works def ex3 : IO Bool := do