From 724903c0a70818d07076feca97f9805936faff77 Mon Sep 17 00:00:00 2001 From: Justus Matthiesen Date: Mon, 20 Nov 2023 18:28:49 +0000 Subject: [PATCH 1/2] [ fix #3143 ] traverse as-patterns in `getImpossibleTerm` --- src/TTImp/Impossible.idr | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/TTImp/Impossible.idr b/src/TTImp/Impossible.idr index 5e034816bc..da6b4052b4 100644 --- a/src/TTImp/Impossible.idr +++ b/src/TTImp/Impossible.idr @@ -157,6 +157,8 @@ mutual Core ClosedTerm mkTerm (IVar fc n) mty exps autos named = buildApp fc n mty exps autos named + mkTerm (IAs fc fc' u n pat) mty exps autos named + = mkTerm pat mty exps autos named mkTerm (IApp fc fn arg) mty exps autos named = mkTerm fn mty (arg :: exps) autos named mkTerm (IAutoApp fc fn arg) mty exps autos named From 21874998b2878aeac836cb387516fc6b725d94bc Mon Sep 17 00:00:00 2001 From: Justus Matthiesen Date: Mon, 20 Nov 2023 18:35:06 +0000 Subject: [PATCH 2/2] [ test ] impossible as-pattern --- tests/idris2/coverage/coverage020/Issue3143.idr | 5 +++++ tests/idris2/coverage/coverage020/expected | 1 + tests/idris2/coverage/coverage020/run | 3 +++ 3 files changed, 9 insertions(+) create mode 100644 tests/idris2/coverage/coverage020/Issue3143.idr create mode 100644 tests/idris2/coverage/coverage020/expected create mode 100755 tests/idris2/coverage/coverage020/run diff --git a/tests/idris2/coverage/coverage020/Issue3143.idr b/tests/idris2/coverage/coverage020/Issue3143.idr new file mode 100644 index 0000000000..dd67f73bb5 --- /dev/null +++ b/tests/idris2/coverage/coverage020/Issue3143.idr @@ -0,0 +1,5 @@ +import Data.Nat + +failing "f is not covering." + f : {n : Nat} -> LT n n -> Void + f x@LTEZero impossible diff --git a/tests/idris2/coverage/coverage020/expected b/tests/idris2/coverage/coverage020/expected new file mode 100644 index 0000000000..d4bcbee66b --- /dev/null +++ b/tests/idris2/coverage/coverage020/expected @@ -0,0 +1 @@ +1/1: Building Issue3143 (Issue3143.idr) diff --git a/tests/idris2/coverage/coverage020/run b/tests/idris2/coverage/coverage020/run new file mode 100755 index 0000000000..686ef2e7a0 --- /dev/null +++ b/tests/idris2/coverage/coverage020/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +check Issue3143.idr