s numeq with type num -> num -> bool
>
> On Thu, Nov 19, 2015 at 7:14 PM, Ramana Kumar
> wrote:
>
>> How about this?
>> Define`issucsuc x y <=> x < y /\ (y - 2 = x)`;
>>
>> On 19 November 2015 at 10:31, Muhammad Nadeem Iqbal
>> wrote:
>&
Define`
> (another_binary_relation T T = F) /\
> (another_binary_relation T F = T) /\
> (another_binary_relation F T = T) /\
> (another_binary_relation F F = F)`;
>
> On 18 November 2015 at 17:01, Muhammad Nadeem Iqbal <
> muhammadnadeemiq...@uoslahore.edu.pk> wrote:
>
>> I h
I have a query that how can we define a binary relation in HOL with a
specified type?
--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lis
