From 5a05e9e8d4d3226e49747e1fa4a4b820ecd46dac Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 22 Dec 2024 08:47:38 +0900 Subject: [PATCH] test: Add binder capturing test --- Test/Frontend.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/Test/Frontend.lean b/Test/Frontend.lean index a3b73ae..2c5809f 100644 --- a/Test/Frontend.lean +++ b/Test/Frontend.lean @@ -193,6 +193,15 @@ def mystery (k: Nat) : Nat := true } ] +def test_capture_type_mismatch_in_binder : TestT MetaM Unit := do + let input := " +example (p: Prop) (h: (∀ (x: Prop), Nat) → p): p := h (λ (y: Nat) => 5) + " + let goalStates ← (collectSorrysFromSource input).run' {} + let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}" + checkEq "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize)) #[ + ] + def collectNewConstants (source: String) : MetaM (List (List Name)) := do let filename := "" let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {} @@ -227,6 +236,7 @@ def suite (env : Environment): List (String × IO LSpec.TestSeq) := ("sorry_in_coupled", test_sorry_in_coupled), ("environment_capture", test_environment_capture), ("capture_type_mismatch", test_capture_type_mismatch), + ("capture_type_mismatch_in_binder", test_capture_type_mismatch_in_binder), ("collect_one_constant", test_collect_one_constant), ("collect_one_theorem", test_collect_one_theorem), ]