max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix test

Browse source
This commit is contained in:
Leonardo de Moura 2020-03-31 10:10:57 -07:00
parent 082b13456c
commit 22fc56f5c8
1 changed files with 0 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
tests/lean/run/generalizeTelescope.lean
View file

@ -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 ()