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

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

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

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

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

open Printf

module type Ord =
sig
  type t
  val lt : t -> t -> bool
  val lte : t -> t -> bool
  val eq : t -> t -> bool
end

voila

open Printf

module type Ord =
sig
  type t
  val lt : t -> t -> bool
  val lte : t -> t -> bool
  val eq : t -> t -> bool
  val succ : t -> t
end

voila

Keybase proof

I hereby claim:

• I am voila on github.
• I am th3rac25 (https://keybase.io/th3rac25) on keybase.
• I have a public key ASCeC9hVEe0BrGoScMK4IAb0V3F8O40tgBLXc6nyxW-_hAo

To claim this, I am signing this object: