--#include "../Prelude.alfa" --#include "New/Datoid/Equality.alfa" open DATOID use Datoid, QD, deqD package DatoidBase where -- Datoid building blocks: public open EqualityDatoid use deqUnit :: Deq SET.Unit , deqSum :: (A::Set)->(B::A -> Set)-> (DA::Deq A)->(DB::(a::A) -> Deq (B a))-> Deq (Sum A B) , deqTimes:: (A::Set)->(B::Set)->(DA::Deq A)->(DB::Deq B)->Deq (SET.Times A B)