mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-17 00:10:31 +03:00
abdadead0a
Only need to match one possibility (it's essentially impossible to match more than one after all!). Fixes #297.
11 lines
336 B
Idris
11 lines
336 B
Idris
data Foobar : String -> Type where
|
|
MkBar : (s : String) -> Foobar s
|
|
|
|
test : (foobar : (x ** Foobar x)) -> String
|
|
test (MkDPair fst snd) with (snd)
|
|
test (MkDPair fst snd) | (MkBar fst) = ?test_rhs__rhs_
|
|
|
|
test' : (foobar : (x ** Foobar x)) -> String
|
|
test' (s ** foobar) with (foobar)
|
|
test' (s ** foobar) | with_pat = ?test'_rhs_rhs
|