From 22fc56f5c85d23cfda606eb9c986ccd0474492b8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 31 Mar 2020 10:10:57 -0700 Subject: [PATCH] chore: fix test --- tests/lean/run/generalizeTelescope.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/tests/lean/run/generalizeTelescope.lean b/tests/lean/run/generalizeTelescope.lean index abe79f60c1..d741ec8b2c 100644 --- a/tests/lean/run/generalizeTelescope.lean +++ b/tests/lean/run/generalizeTelescope.lean @@ -17,7 +17,6 @@ let n1 := mkApp succ n; let vecN1 := mkApp2 (mkConst `Vec) nat n1; withLocalDecl `xs vecN1 BinderInfo.default $ fun xs => do generalizeTelescope #[n1, xs] `aux $ fun ys => do -let ys := (ys.map mkFVar); t ← mkLambda ys ys.back; trace! `Meta.debug t; pure () @@ -33,7 +32,6 @@ let vecN1 := mkApp2 (mkConst `Vec) nat n1; withLocalDecl `xs vecN1 BinderInfo.default $ fun xs => do e ← mkEqRefl xs; generalizeTelescope #[n1, xs, e] `aux $ fun ys => do -let ys := (ys.map mkFVar); t ← mkLambda ys ys.back; trace! `Meta.debug t; pure () @@ -52,7 +50,6 @@ withLocalDecl `xs vecN1 BinderInfo.default $ fun xs => do e ← mkEqRefl xs; failIfSuccess $ do { generalizeTelescope #[n1, e] `aux $ fun ys => do - let ys := (ys.map mkFVar); t ← mkLambda ys ys.back; trace! `Meta.debug t; pure ()