From fbb858a32cee8090e5390df1fb688b032148645b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 8 Aug 2022 23:40:44 -0700 Subject: [PATCH] chore: missing case --- tests/playground/simpleTypes.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/tests/playground/simpleTypes.lean b/tests/playground/simpleTypes.lean index 11b123f900..176231c4aa 100644 --- a/tests/playground/simpleTypes.lean +++ b/tests/playground/simpleTypes.lean @@ -17,6 +17,11 @@ partial def simpType (type : Expr) : MetaM Expr := do match type with | .sort u => return .sort u | .const .. => visitApp type #[] + | .lam n d b bi => + withLocalDecl n bi d fun x => do + let d ← simpType d + let b ← simpType (b.instantiate1 x) + return .lam n d (b.abstract #[x]) bi | .forallE n d b bi => withLocalDecl n bi d fun x => do let borrowed := isMarkedBorrowed d