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

[François Thiré]

Exactly! I was confused between *constants* and *type operators*.

Thanks a lot!

Cheers,

François

2017-01-11 19:56 GMT+01:00 Joe Leslie-Hurd <joe at gilith.com>:

> 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
> >
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20170111/08c98d8e/attachment.html>