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
