From 75f166edccfe3adb3d664080b250b204f3f25c83 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 14 Sep 2022 13:59:09 -0700 Subject: [PATCH] feat: add `assertNoFun` test --- src/Lean/Compiler/LCNF/Testing.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/Lean/Compiler/LCNF/Testing.lean b/src/Lean/Compiler/LCNF/Testing.lean index 9b1bec490c..fdbaa252ae 100644 --- a/src/Lean/Compiler/LCNF/Testing.lean +++ b/src/Lean/Compiler/LCNF/Testing.lean @@ -233,5 +233,12 @@ Assert that the pass under test produces `Decl`s that do not contain def assertDoesNotContainConstAfter (constName : Name) (msg : String) : TestInstaller := assertForEachDeclAfterEachOccurence (fun _ decl => !decl.value.containsConst constName) msg +def assertNoFun : TestInstaller := + assertAfter do + for decl in (← getDecls) do + decl.value.forM fun + | .fun .. => throwError "declaration `{decl.name}` contains a local function declaration" + | _ => return () + end Testing end Lean.Compiler.LCNF