git.iko.soy/Idris-dev
on master help sign in
Remove hole in interfaces002
73d4721Edwin Brady
test/interfaces002/expected−4
compare with master
unifiedsplit
@@ -1,5 +1 @@
1−WARNING: There are incomplete holes:
2− [Main.prf]
3−
4−Evaluation of any of these will crash at run time.
541
141
test/interfaces002/interfaces002.idr+1−1
@@ -34,6 +34,6 @@ testSum : Array n Int -> Int
34testSum = sumArray
34testSum = sumArray
35
35
36main : IO ()
36main : IO ()
37−main = printLn (testSum (upd 11 2 ?prf (create 4 10)))
37+main = printLn (testSum (upd 11 1 (LTESucc (LTESucc LTEZero)) (create 4 10)))
38
38
39
39