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

[Joe Leslie-Hurd]

Hi Francois,

It sounds like you want to define a new *constant* with type A -> A ->
bool, not a new type operator, but perhaps I am missing something?

Cheers,

Joe

On Wed, Jan 11, 2017 at 9:47 AM, François Thiré <franth2 at gmail.com> wrote:
> 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
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>