It seems like a bad idea to use the same “where” syntax for definitions and test cases, especially since a major aim of this is education.