voila

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

voila

(* "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 *)

voila

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

voila

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

voila

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

voila

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]}

voila

%% 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)))).

voila

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

voila

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]).

voila

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