git.iko.soy/Idris-dev
on master help sign in
Fixed some tests broken under renaming
commit8f54aaf1b893527e388f09db852dea280dceba82 authorAhmad Salim Al-Sibahi <asal@itu.dk> dateThu 25 Sep 2014, 20:34 (12 years ago) parentfe569c4
3 files changed+14−14
compare with master
unifiedsplit
test/basic005/test019.lidr+6−6 test/basic010/Main.idr+2−2 test/effects002/test025.idr+6−6
test/basic005/test019.lidr+6−6
@@ -1,16 +1,16 @@
11> module Main
22
3−> ifTrue : so True -> Nat
4−> ifTrue oh = S Z
3+> ifTrue : So True -> Nat
4+> ifTrue Oh = S Z
55
6−> ifFalse : so False -> Nat
7−> ifFalse oh impossible
6+> ifFalse : So False -> Nat
7+> ifFalse Oh impossible
88
9−> test : (f : Nat -> Bool) -> (n : Nat) -> so (f n) -> Nat
9+> test : (f : Nat -> Bool) -> (n : Nat) -> So (f n) -> Nat
1010> test f n x with (f n)
1111> | True = ifTrue x
1212> | False = ifFalse x
1313
1414> main : IO ()
15−> main = print (test ((S 4) ==) 5 oh)
15+> main = print (test ((S 4) ==) 5 Oh)
1616
test/basic010/Main.idr+2−2
@@ -20,7 +20,7 @@ eq_refl {n = S n} = eqS eq_refl
2020-- Here, the proof is very expensive to compute.
2121-- We add a recursive argument to prevent Idris from inlining the function.
2222f : (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
2424f (S r) n = f r n
2525
2626-- A (contrived) relation, just to have something to show.
@@ -30,7 +30,7 @@ data represents : Nat -> Nat -> Type where
3030-- Here, the witness is very expensive to compute.
3131-- We add a recursive argument to prevent Idris from inlining the function.
3232g : (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)
3434g (S r) n = g r n
3535
3636fmt : 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
1616
1717testMemory : MemoryIO () () (Vect 4 Int)
1818testMemory = do Src :- allocate 5
19− Src :- poke 0 inpVect oh
19+ Src :- poke 0 inpVect Oh
2020 Dst :- allocate 5
21− Dst :- initialize (prim__truncInt_B8 1) 2 oh
22− move 2 2 3 oh oh
21+ Dst :- initialize (prim__truncInt_B8 1) 2 Oh
22+ move 2 2 3 Oh Oh
2323 Src :- free
24− end <- Dst :- peek 4 (S Z) oh
25− Dst :- poke 4 (sub1 end) oh
26− res <- Dst :- peek 1 (S(S(S(S Z)))) oh
24+ end <- Dst :- peek 4 (S Z) Oh
25+ Dst :- poke 4 (sub1 end) Oh
26+ res <- Dst :- peek 1 (S(S(S(S Z)))) Oh
2727 Dst :- free
2828 return (map (prim__zextB8_Int) res)
2929