default assert.eq.c = assert.eqable.t;
default arbitrary.c =
gen.arbitraryable.t,
assert.eqable.t,
assert.orderable.t,
;
module 'gen.arbitraryable ∝ data. | it;
instance arbitrary.c gen.arbitraryable.t = constr gen.arbitraryable.it;
instance function.arbitrary.c gen.arbitraryable.t 'gen = map const gen;
module 'eqable ∝ data. | one | other;
instance arbitrary.c assert.eqable.t =
<|> constr assert.eqable.one
<|> constr assert.eqable.other
;
instance assert.eq.c eqable.t eqable.one eqable.one :- true log{§gs{one} ≡ §gs{one}};
instance assert.eq.c eqable.t eqable.one eqable.other :- false log{§gs{one} ≠ §gs{other}};
instance assert.eq.c eqable.t eqable.other eqable.one :- false log{§gs{other} ≠ §gs{one}};
instance assert.eq.c eqable.t eqable.other eqable.other :- true log{§gs{other} ≡ §gs{other}};
module function.arbitrary ∝ newoverload 'α.
∀ 'β. arbitrary.t β → arbitrary.t (α → β)
;
instance arbitrary.c ('α → 'β) | arbitrary.c β, function.arbitrary.c α = function.arbitrary arbitrary;
either.function.arbitrary :: ∀ 'α 'β. function.arbitrary.t α → function.arbitrary.t β →
function.arbitrary.t (either.t α β)
;
'either.function.arbitrary 'fl 'fr 'gen =
<|> const <$> gen
<|> constr either <*> fl gen <*> fr gen
;
maybe.function.arbitrary :: ∀ 'α. function arbitrary.t α → function.arbitrary.t (maybe.t α);
'maybe.function.arbitrary 'f 'gen =
<|> const <$> gen
<|> constr maybe <*> gen <*> f gen
;
'list.function.arbitrary 'f 'gen =
<|> const gen
<|> promote (for ('z ← gen; 'op ← f $ list.function.arbitrary f $ gen;)
unit $ λ 'xn. analyze xn
case nil. z
case 'x:'xn1. op x xn1
)
;
instance assert.eq.c (list.t 'α) | assert.eq.c α, list.fmtgs.c α, = w
(where
'w nil nil :- true log{§gs{nil ≡ nil}};
'w ('x:'xn) nil :- property.false log{§gs(fmtgs (x:xn)) ≠ nil};
'w nil ('y:'ys) :- property.false log{nil ≠ §gs(fmtgs (y:ys))};
'w ('x:'xn) ('y:'ys) :- assert.eq x y ∧ delay.not.proven w xn ys;
)
;