ac.why 230 Bytes
Newer Older
1
2
theory Test
       type t
Andrei Paskevich's avatar
Andrei Paskevich committed
3
       function f t t : t
4
       clone algebra.AC with type t = t, function op = f, axiom .
Andrei Paskevich's avatar
Andrei Paskevich committed
5
       goal G1 : forall x y : t. f x y = f y x
Andrei Paskevich's avatar
Andrei Paskevich committed
6
       goal G2 : forall x y z : t. f (f x y) z = f x (f y z)
7
end