<div dir="ltr"><div><div><div>Hi,<br><br></div>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.<br><br></div>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. <br><br></div><div>So I'm wondering how can I achieve that using the article format? Obviously, I am missing something... <br><br></div><div>Have a nice day,<br></div><div><br></div><div>François<br></div></div>