How about this? Define`issucsuc x y <=> x < y /\ (y - 2 = x)`; On 19 November 2015 at 10:31, Muhammad Nadeem Iqbal <muhammadnadeemiq...@uoslahore.edu.pk> wrote: > in your first example, you have specified two constants to x and y. Mine is > a bit different case. I want the one in which there should not be such > specification. > > On Wed, Nov 18, 2015 at 10:28 PM, Ramana Kumar <ram...@member.fsf.org> > wrote: >> >> Which binary relation? What do you mean? >> >> Here's a binary relation that relates natural numbers 1 and 2: >> val a_binary_relation_def = Define`a_binary_relation x y <=> (x = 1) /\ (y >> = 2)`; >> >> Here's a binary relation that relates two Booleans iff exactly one of them >> is true: >> val another_binary_relation_def = 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 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/lists/listinfo/hol-info >>> >> > > > ------------------------------------------------------------------------------ > > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info >
------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
