[opentheory-users] Define n-ary type operators using the article format
franth2 at gmail.com
Wed Jan 11 17:47:15 UTC 2017
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
So I'm wondering how can I achieve that using the article format?
Obviously, I am missing something...
Have a nice day,
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the opentheory-users