mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-19 19:01:44 +03:00
fd4f90e331
This required a small change to auto implicit search (and I'm still not sure about this). Now search arguments right to left, because solving later arguments may resolve earlier arguments by unification and this can happen in particular when chasing parent interfaces (which may have fewer parameters).
25 lines
611 B
Idris
25 lines
611 B
Idris
showIfEq : (Show a, Eq a) => a -> a -> String
|
|
showIfEq x y = if x == y then show x else "Nope"
|
|
|
|
topeq : Eq a => a -> a -> Bool
|
|
topeq x y = x == y
|
|
|
|
data Foo = MkFoo | MkBar
|
|
|
|
-- Should only show the first interface search failure in the tuple
|
|
-- (Ideally it would keep going and find all the failures, but that is
|
|
-- hard to achieve and this way is better than displaying the whole
|
|
-- top level search when only part of it is relevant)
|
|
|
|
test : Int -> String
|
|
test x = showIfEq MkFoo MkBar
|
|
|
|
Eq Foo where
|
|
MkFoo == MkFoo = True
|
|
MkBar == MkBar = True
|
|
_ == _ = False
|
|
|
|
test2 : String
|
|
test2 = showIfEq MkFoo MkBar
|
|
|