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-08-13 14:59:37 -07:00
parent 8b0a100e21
commit a670de93cd
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/lean/run/depElim1.lean
View file

@ -66,7 +66,7 @@ partial def mkPattern : Expr → MetaM Pattern
ps ← ps.toList.mapM mkPattern;
pure $ Pattern.arrayLit type ps
else match e.arrayLit? with
| some es => do
| some (_, es) => do
pats ← es.mapM mkPattern;
type ← inferType e;
type ← whnfD type;
@ -99,7 +99,7 @@ partial def decodeAltLHS (e : Expr) : MetaM AltLHS :=
forallTelescopeReducing e fun args body => do
decls ← args.toList.mapM (fun arg => getLocalDecl arg.fvarId!);
pats ← decodePats body;
pure { fvarDecls := decls, patterns := pats }
pure { localDecls := decls, patterns := pats }
partial def decodeAltLHSs : Expr → MetaM (List AltLHS)
| e =>