Often when I switch between Racket, my home language, and Coq, a research interest, I am struck by a minor but meaningful difference: Racket allows functions that vary in how many arguments they take, and Coq does not. It's minor, but it means that, for example, I cannot use this idiom: (map + '(1 2 3) '(4 5 6) '(7 8 9)) ⇝ '(12 15 18) This works because in Racket, + takes any number of arguments and adds them all, and map takes any number of lists as arguments (it picks one element from eac...
