Enigma example in "Programming Cryptol" needs to be updated

[smithdtyler]

In section 3.2, the call to elem in mkRotor is incorrect, as elem does not take a tuple.

mkRotor : {n} (fin n) => (Permutation, String n) -> Rotor
mkRotor (perm, notchLocations) = [ (p, elem (p, notchLocations))
| p <- perm
]

Should be

mkRotor (perm, notchLocations) = [ (p, elem p notchLocations)
                                | p <- perm
                                ]

[sauclovian-g]

It's more complicated than that since this elem is a private definition (see line 762 of Enigma.tex for the copy that's used here) so one should change not just this usage, but also that definition and also the real one elsewhere in the book that the comment about an exercise refers to. And there are other references scattered around the book, some of which use one signature and some the other, and they should probably all be updated as well.

Is there any reason that one would deliberately use a different type signature for the exercise version? Or is it all just Olde?

[yav]

I think in old Cryptol things used to take tuples as arguments more often, because a long time ago there was an idea that maybe Cryptol could kind of look like C. So, quite likely, this falls directly in the "olde" category.