[opentheory-users] Define n-ary type operators using the article format

[François Thiré]

Hi,

I'm new in the world of HOL/Opentheory and I'm running into some
difficulties. I don't understand how it is possible to define n-ary type
operators using the article format.

Let us say for example that I want to encode Leibniz equality. Then this
equality will be a type operator of type A -> A -> bool. To declare a new
type operator, I have to use the command "defineTypeOp". Though, this
latter takes a unary predicate where I think I would need a binary
predicate.

So I'm wondering how can I achieve that using the article format?
Obviously, I am missing something...

Have a nice day,

François
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20170111/9e495e3c/attachment.html>