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 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
  val succ : t -> t
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
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:

voila

/* Impose an ordering on the State. */
open util/ordering[State]
open util/integer

/* Stores the jugs level */
sig State { small, big:Int }

/* initial state */
fact { first.small = 0 && first.big = 0 }