Obviously the branch was done quickly, but at a short glance it was easier not to use an extra line to add `open Num` at the beginning.

Good call on the irc channel. Thanks!