diff --git a/src/TTImp/Interactive/CaseSplit.idr b/src/TTImp/Interactive/CaseSplit.idr index edd6283f12..e741314556 100644 --- a/src/TTImp/Interactive/CaseSplit.idr +++ b/src/TTImp/Interactive/CaseSplit.idr @@ -197,7 +197,7 @@ newLHS : {auto c : Ref Ctxt Defs} -> newLHS fc envlen allvars var con tm = do let (f, args) = getFnArgs tm [] let keep = map (const (Explicit fc (Implicit fc True))) - (take envlen args) + (mapMaybe isExplicit $ take envlen args) let ups = drop envlen args ups' <- traverse (update allvars var con) ups pure $ apply f (keep ++ ups') diff --git a/tests/Main.idr b/tests/Main.idr index 6d36a63475..4718724b1f 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -132,7 +132,7 @@ idrisTests = MkTestPool "Misc" [] Nothing -- Namespace blocks "namespace001", "namespace002", "namespace003", "namespace004", "namespace005", -- Parameters blocks - "params001", "params002", "params003", + "params001", "params002", "params003", "params004", -- Larger programs arising from real usage. Typically things with -- interesting interactions between features "real001", "real002", diff --git a/tests/idris2/misc/params004/Issue2331.idr b/tests/idris2/misc/params004/Issue2331.idr new file mode 100644 index 0000000000..2c7d5b5d55 --- /dev/null +++ b/tests/idris2/misc/params004/Issue2331.idr @@ -0,0 +1,5 @@ +parameters {auto _ : ()} + + f : Nat -> Nat + f m = ?a + diff --git a/tests/idris2/misc/params004/expected b/tests/idris2/misc/params004/expected new file mode 100644 index 0000000000..71101b68ce --- /dev/null +++ b/tests/idris2/misc/params004/expected @@ -0,0 +1,4 @@ +1/1: Building Issue2331 (Issue2331.idr) +Main> f 0 = ?a_0 + f (S k) = ?a_1 +Main> Bye for now! diff --git a/tests/idris2/misc/params004/input b/tests/idris2/misc/params004/input new file mode 100644 index 0000000000..d15961bf91 --- /dev/null +++ b/tests/idris2/misc/params004/input @@ -0,0 +1,2 @@ +:cs 4 5 m +:q diff --git a/tests/idris2/misc/params004/run b/tests/idris2/misc/params004/run new file mode 100644 index 0000000000..4044d72b7e --- /dev/null +++ b/tests/idris2/misc/params004/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +idris2 Issue2331.idr < input