1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski%% Type Constructors -----------------------------------------------------

1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowskis : Type

1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowskit : Type

c06dd8856a03b72f6b3f69e874f8700f10cb8522Christian Maeder%% Assumptions -----------------------------------------------------------

f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski__+__ : t -> t -> t

c06dd8856a03b72f6b3f69e874f8700f10cb8522Christian Maeder : t � t -> t

c06dd8856a03b72f6b3f69e874f8700f10cb8522Christian Maeder : s � s -> s

1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski : s -> s -> s,idem, assoc, comm

1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowskia : t

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski : s

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederb : t

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder : s

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederc : s = a + b

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder%% Diagnostics -----------------------------------------------------------

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederHint (line 5, column 14) type 's � s' is not unifiable with 's'

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederHint (line 7, column 14) type 't' is not unifiable with 's'

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederHint (line 5, column 14) type 't � t' is not unifiable with 's'

c06dd8856a03b72f6b3f69e874f8700f10cb8522Christian MaederHint (line 8, column 14) type 't' is not unifiable with 't � t'

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederHint (line 7, column 14) type 't' is not unifiable with 's � s'

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederHint (line 5, column 14) type 't' is not unifiable with 's'

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederHint (line 3, column 12) type 't' is not unifiable with 's'

c0ba7121c93e4f9292f2d95a0ac7460a7b9e5aeaTill MossakowskiHint (line 3, column 12) type 't' is not unifiable with 's'

e3c9174a782e90f965a0b080c22861c3ef5af12dTill MossakowskiError (line 13, column 12) ambiguous mixfix term: a + b

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (op __+ : s -> s -> s) (op a : s) (op b : s)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (op __+__ : s � s -> s) ((op a : s), (op b : s))

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder