Re: [isabelle] bijections to/from the natural numbers
Florian Haftmann wrote:
I have only one comment: the standard naming scheme should be (as in
foo_of_bar :: bar => foo
I think this naming scheme would be inappropriate here, since it hints
at some kind of "obvious conversion". For example, the function
nat_to_int_bij is defined as
nat_to_int_bij n = (if 2 dvd n then int(n div 2) else -int(Suc n div 2))
Naming it "int_of_nat" would be confusing IMO.
I added pair_encode together with class "countable" around 2007, not
knowing about the others. I think that function is only used to derive
the class instance, so it can safely be replaced by any other definition...
Other naming suggestions:
cantor_pair :: "nat * nat => nat"
cantor_unpair :: "nat => nat * nat"
This archive was generated by a fusion of
Pipermail (Mailman edition) and