mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-11 13:36:08 +03:00
[ fix ] case spliting under implicit/auto parameter
This commit is contained in:
parent
f8adee7059
commit
055568be28
@ -197,7 +197,7 @@ newLHS : {auto c : Ref Ctxt Defs} ->
|
|||||||
newLHS fc envlen allvars var con tm
|
newLHS fc envlen allvars var con tm
|
||||||
= do let (f, args) = getFnArgs tm []
|
= do let (f, args) = getFnArgs tm []
|
||||||
let keep = map (const (Explicit fc (Implicit fc True)))
|
let keep = map (const (Explicit fc (Implicit fc True)))
|
||||||
(take envlen args)
|
(mapMaybe isExplicit $ take envlen args)
|
||||||
let ups = drop envlen args
|
let ups = drop envlen args
|
||||||
ups' <- traverse (update allvars var con) ups
|
ups' <- traverse (update allvars var con) ups
|
||||||
pure $ apply f (keep ++ ups')
|
pure $ apply f (keep ++ ups')
|
||||||
|
@ -132,7 +132,7 @@ idrisTests = MkTestPool "Misc" [] Nothing
|
|||||||
-- Namespace blocks
|
-- Namespace blocks
|
||||||
"namespace001", "namespace002", "namespace003", "namespace004", "namespace005",
|
"namespace001", "namespace002", "namespace003", "namespace004", "namespace005",
|
||||||
-- Parameters blocks
|
-- Parameters blocks
|
||||||
"params001", "params002", "params003",
|
"params001", "params002", "params003", "params004",
|
||||||
-- Larger programs arising from real usage. Typically things with
|
-- Larger programs arising from real usage. Typically things with
|
||||||
-- interesting interactions between features
|
-- interesting interactions between features
|
||||||
"real001", "real002",
|
"real001", "real002",
|
||||||
|
5
tests/idris2/misc/params004/Issue2331.idr
Normal file
5
tests/idris2/misc/params004/Issue2331.idr
Normal file
@ -0,0 +1,5 @@
|
|||||||
|
parameters {auto _ : ()}
|
||||||
|
|
||||||
|
f : Nat -> Nat
|
||||||
|
f m = ?a
|
||||||
|
|
4
tests/idris2/misc/params004/expected
Normal file
4
tests/idris2/misc/params004/expected
Normal file
@ -0,0 +1,4 @@
|
|||||||
|
1/1: Building Issue2331 (Issue2331.idr)
|
||||||
|
Main> f 0 = ?a_0
|
||||||
|
f (S k) = ?a_1
|
||||||
|
Main> Bye for now!
|
2
tests/idris2/misc/params004/input
Normal file
2
tests/idris2/misc/params004/input
Normal file
@ -0,0 +1,2 @@
|
|||||||
|
:cs 4 5 m
|
||||||
|
:q
|
3
tests/idris2/misc/params004/run
Normal file
3
tests/idris2/misc/params004/run
Normal file
@ -0,0 +1,3 @@
|
|||||||
|
. ../../../testutils.sh
|
||||||
|
|
||||||
|
idris2 Issue2331.idr < input
|
Loading…
Reference in New Issue
Block a user