git.iko.soy/Idris-dev
on master help sign in
Search open instances first

Otherwise we'll find the default if it exists, and that's not what we want.

commit37aa54a868da1d1269a92dc42ee336e394e3896f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 8 May 2016, 20:07 (10 years ago) parent254a227
3 files changed+22−4
compare with master
unifiedsplit
src/Idris/ProofSearch.hs+1−1 test/interfaces004/expected+2 test/interfaces004/interfaces004.idr+19−3
src/Idris/ProofSearch.hs+1−1
@@ -392,7 +392,7 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist
392392 try' (trivialTCs okholes elab ist)
393393 (do addDefault t tc ttypes
394394 let stk = map fst (filter snd $ elab_stack ist)
395− let insts = findInstances ist t ++ idris_openimpls ist
395+ let insts = idris_openimpls ist ++ findInstances ist t
396396 blunderbuss t depth stk (stk ++ insts)) True
397397
398398 -- returns Just hs if okay, where hs are holes which are okay in the
test/interfaces004/expected+2
@@ -1,2 +1,4 @@
1112
2236
3+True
4+False
test/interfaces004/interfaces004.idr+19−3
@@ -14,6 +14,22 @@
1414test : Monoid a => a -> a
1515test x = x <+> x <+> neutral
1616
17−main : IO ()
18−main = do printLn (test @{PlusNatMonoid} 6)
19− printLn (test @{MultNatMonoid} 6)
17+[CmpLess] Ord Int where
18+ compare x y = if (x == y) then EQ else
19+ if (boolOp prim__sltInt x y) then GT else LT
20+
21+foo : Int -> Int -> Bool
22+foo x y = x < y
23+
24+using implementation CmpLess
25+ foo' : Int -> Int -> Bool
26+ foo' x y = x < y
27+
28+using implementation PlusNatMonoid
29+ main : IO ()
30+ main = do printLn (test (the Nat 6))
31+ printLn (test @{MultNatMonoid} 6)
32+
33+ printLn (foo 3 4)
34+ printLn (foo' 3 4)
35+