Skip to content

Instantly share code, notes, and snippets.

voila

  • Dunedin, NZ
Block or report user

Report or block voila

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
View okasaki2.2.ml
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
View okasaki2.1.ml
(* "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 *)
View stack.idr
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
View index.idr
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
View depdate.hs
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
View proper5
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]}
View duplist.erl
%% 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)))).
View proper4
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
View delete_all2.erl
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]).
View proper3
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
You can’t perform that action at this time.