Функция возвращает «Нет решения» вместо «Ничего»

У меня есть стандартный тип данных, представляющий формулы логики предикатов. Функция, представляющая правило исключения естественного вывода для дизъюнкции, может выглядеть так:

d_el p q =
  if p =: (Dis r s) && q =: (Neg r) then Just s else
  if q =: (Dis r s) && p =: (Neg r) then Just s else
     Nothing where r,s free

x =: y = (x =:= y) == success

Вместо того, чтобы оценивать значение Nothing, когда объединение не удается, функция не возвращает никаких решений в PACKS :

logic> d_el (Dis Bot Top) (Not Bot)
Result: Just Top
More Solutions? [Y(es)/n(o)/a(ll)] n
logic> d_el (Dis Bot Top) (Not Top)
No more solutions.

Что мне не хватает и почему не el вычисляет Ничего при сбое объединения?

9
задан danportin 3 December 2011 в 05:20
поделиться