Hi Michael,
thanks for detailed explanations. Then I guess I should choose another name for
the conflicted symbols in the PR.
—Chun
> Il giorno 28 mag 2018, alle ore 11:55,
> ha scritto:
>
> The two definitions are not equivalent. The BIJ overload permits functions
> to be designated perm
The two definitions are not equivalent. The BIJ overload permits functions to
be designated permutations that the definition does not. BIJ can be used to
identify bijections between different types so it can't/shouldn't require
anything much of functions outside their domain. I think one's cho
Hi,
(I’m trying to convert the current pending PR into acceptable code changes)
in pred_setTheory, I saw there’s a definition of PERMUTES (permutation
functions over a set) as overloading of BIJ (bijections):
val _ = overload_on("PERMUTES", ``\f s. BIJ f s s``);
val _ = set_fixity "PERMUTES" (I
