mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-22 19:21:39 +03:00
a972778eab
They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
10 lines
301 B
Idris
10 lines
301 B
Idris
interface Foo m where
|
|
bar : k -> v -> m k v -> m k v
|
|
|
|
-- This is kind of meaningless, except it exposes a potential error where
|
|
-- (\s, t => List (s, t)) is substituted in as 'm' in 'm k v' and the ks
|
|
-- clash, so one has to be renamed.
|
|
Eq k => Foo (\s, t => List (s, t)) where
|
|
bar x y z = ?bang
|
|
|