tests.makam

%use "init".

categorical : testsuite.
%testsuite categorical.

(* Check Basic Numbers Work *)
>> eval << 1 >> Dom Cod Result ?
>> Yes:
>> Result := "5 ",
>> Cod := "Z ",
>> Dom := "* ".

(* Check Basic Addition Works *)
>> eval << (add lift 4) lift 8 >> Dom Cod Result ?
>> Yes:
>> Result := "12 ",
>> Range := "Z ",
>> Domain := "* ".

(* Check Identity Works *)
>> eval << lam "a" : * -> Set => lam "x" : * -> "a" => "x" >> Dom Cod Result ?
>> Yes:
>> Cod := "exists \"x1\" : * -> Set , exists \"x2\" : * -> \"x1\" , \"x1\" ",
>> Dom := "* ".

(* Check Axioms Work *)
>> eval {
>> Let "myaxiom" := axiom "myaxiom" : Z -> Z .
>> "myaxiom"
>> } Dom Cod Result ?
>> Yes:
>> Cod := "Z ",
>> Dom := "Z ".

>> eval << 1 >> Dom Cod Result ?
>> Yes:
>> Result := "1 ".

>> eval << lam "a" : * -> Set => "a" >> Dom Cod Result ?
>> Yes:
>> Result := "lam \"x1\" : * -> Set => \"x1\" ∘ ! term ".

>> eval << id Z ∘ 1 >> Dom Cod Result ?
>> Yes:
>> Result := "1 ".

(* FIXME demonstrate more forall/exists stuff *)
(* FIXME experiment with coforall/coexists *)