This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module type Ord = | |
sig | |
type t | |
val lt : t -> t -> bool | |
val lte : t -> t -> bool | |
val eq : t -> t -> bool | |
end | |
module IntOrd : Ord with type t = int = | |
struct |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* "comparable" interface *) | |
module type Ord = | |
sig | |
type t | |
val lt : t -> t -> bool | |
val lte : t -> t -> bool | |
val eq : t -> t -> bool | |
end | |
(* implementation of Ord for integers *) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Main | |
PosInt : Type | |
PosInt = Nat | |
data Inst : PosInt -> PosInt -> Type where | |
PUSH : (v:Int) -> Inst n (1 + n) | |
ADD : Inst (2 + n) (1 + n) | |
data Prog : PosInt -> PosInt -> Type where |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Main | |
-- Type for unit tests | |
Test : Bool -> Type | |
Test = so | |
-- ok has type (Test b), whenever b evaluates to True | |
ok : Test True | |
ok = oh |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Date | |
-- leap year ? | |
leap : Integer -> Bool | |
leap year = (mod year 4 == 0) && ((mod year 400 == 0) || not (mod year 100 == 0)) | |
-- number of days in month/year | |
days : Integer -> Integer -> Integer | |
days 2 year = if leap year then 29 else 28 | |
days month _ = if month `List.elem` [4,6,9,11] then 30 else 31 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
10% {0,[]} | |
10% {0,[9,37,9,37]} | |
10% {3,[]} | |
10% {7,[-6,2,8,-31,56,5,-3,20,37,51,-21,4,-10,43,9,-61,16,-4,33,-6,2,8,-31,56,5,-3,20,37,51,-21,4,-10,43,9,-61,16,-4,33]} | |
10% {13,[14,6,3,-7,14,6,3,-7]} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
%% custom generator for lists of duplicates | |
duplist(Type) -> | |
?LET(L,list(Type), | |
L ++ L). | |
prop_delete6() -> | |
?FORALL({X,L}, | |
{integer(), duplist(integer())}, %% our custom generator | |
collect({X, L}, %% show us the X and L generated | |
not lists:member(X, delete_all(X, L)))). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
4> proper:quickcheck(listdel:prop_delete3()). | |
.xx..xxx........................x.....x............x...........................x.........x..........x....x...... | |
OK: Passed 100 test(s). | |
true | |
5> proper:quickcheck(listdel:prop_delete3(), 1000). | |
xxx..xx...x.xxxx..xxx.xx...x..xxxx.........x.x.........x...x..........x......x.......x....x...xx...x........x......x......x....x.......x.................x....x......x...........x.......x.....x.x..........x........x.x.................x..x.......................x..........x............x.......x......................................x.......................................x.......x.........x..x...................x..................................................................................x........x.....x..........................................................................x..x.......x..................................x......................x........x..................x...x.........x.x.....................................x.x...........................................x |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
delete_all(_, [], Acc) -> | |
lists:reverse(Acc); | |
delete_all(X, [X|Rest], Acc) -> | |
delete_all(X, Rest, Acc); | |
delete_all(X, [Y|Rest], Acc) -> | |
delete_all(X, Rest, [Y|Acc]). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
27> proper:quickcheck(listdel:prop_delete3()). | |
..x.x.....x...............! | |
Failed: After 24 test(s). | |
[13,13,59,10,11,24,-3,0,4] | |
13 | |
Shrinking ...(3 time(s)) | |
[13,13] | |
13 | |
false |