git.iko.soy/Idris-dev
on master help sign in
Fixed some tests broken under renaming
8f54aafAhmad Salim Al-Sibahi
test/basic005/test019.lidr+6−6
compare with master
unifiedsplit
@@ -1,16 +1,16 @@
1> module Main
1> module Main
2
2
3−> ifTrue : so True -> Nat
3+> ifTrue : So True -> Nat
4−> ifTrue oh = S Z
4+> ifTrue Oh = S Z
5
5
6−> ifFalse : so False -> Nat
6+> ifFalse : So False -> Nat
7−> ifFalse oh impossible
7+> ifFalse Oh impossible
8
8
9−> test : (f : Nat -> Bool) -> (n : Nat) -> so (f n) -> Nat
9+> test : (f : Nat -> Bool) -> (n : Nat) -> So (f n) -> Nat
10> test f n x with (f n)
10> test f n x with (f n)
11> | True = ifTrue x
11> | True = ifTrue x
12> | False = ifFalse x
12> | False = ifFalse x
13
13
14> main : IO ()
14> main : IO ()
15−> main = print (test ((S 4) ==) 5 oh)
15+> main = print (test ((S 4) ==) 5 Oh)
16
16
test/basic010/Main.idr+2−2
@@ -20,7 +20,7 @@ eq_refl {n = S n} = eqS eq_refl
20-- Here, the proof is very expensive to compute.
20-- Here, the proof is very expensive to compute.
21-- We add a recursive argument to prevent Idris from inlining the function.
21-- We add a recursive argument to prevent Idris from inlining the function.
22f : (r, n : Nat) -> Subset Nat (\k => qib n `equals` qib k)
22f : (r, n : Nat) -> Subset Nat (\k => qib n `equals` qib k)
23−f Z n = element n eq_refl
23+f Z n = Element n eq_refl
24f (S r) n = f r n
24f (S r) n = f r n
25
25
26-- A (contrived) relation, just to have something to show.
26-- A (contrived) relation, just to have something to show.
@@ -30,7 +30,7 @@ data represents : Nat -> Nat -> Type where
30-- Here, the witness is very expensive to compute.
30-- Here, the witness is very expensive to compute.
31-- We add a recursive argument to prevent Idris from inlining the function.
31-- We add a recursive argument to prevent Idris from inlining the function.
32g : (r, n : Nat) -> Exists (\k : Nat => k `represents` n)
32g : (r, n : Nat) -> Exists (\k : Nat => k `represents` n)
33−g Z n = evidence (qib n) (axiom n)
33+g Z n = Evidence (qib n) (axiom n)
34g (S r) n = g r n
34g (S r) n = g r n
35
35
36fmt : qib n `represents` n -> String
36fmt : qib n `represents` n -> String
test/effects002/test025.idr+6−6
@@ -16,14 +16,14 @@ sub1 xs = map (prim__truncInt_B8 . (\ x => x - 1) . prim__zextB8_Int) xs
16
16
17testMemory : MemoryIO () () (Vect 4 Int)
17testMemory : MemoryIO () () (Vect 4 Int)
18testMemory = do Src :- allocate 5
18testMemory = do Src :- allocate 5
19− Src :- poke 0 inpVect oh
19+ Src :- poke 0 inpVect Oh
20 Dst :- allocate 5
20 Dst :- allocate 5
21− Dst :- initialize (prim__truncInt_B8 1) 2 oh
21+ Dst :- initialize (prim__truncInt_B8 1) 2 Oh
22− move 2 2 3 oh oh
22+ move 2 2 3 Oh Oh
23 Src :- free
23 Src :- free
24− end <- Dst :- peek 4 (S Z) oh
24+ end <- Dst :- peek 4 (S Z) Oh
25− Dst :- poke 4 (sub1 end) oh
25+ Dst :- poke 4 (sub1 end) Oh
26− res <- Dst :- peek 1 (S(S(S(S Z)))) oh
26+ res <- Dst :- peek 1 (S(S(S(S Z)))) Oh
27 Dst :- free
27 Dst :- free
28 return (map (prim__zextB8_Int) res)
28 return (map (prim__zextB8_Int) res)
29
29