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

Joe Leslie-Hurd joe at gilith.com
Wed Jan 11 18:56:10 UTC 2017

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?



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

More information about the opentheory-users mailing list