Post #2625405

Funky differential operators show up a lot in CS103, because I love them. In Sem 1, we do the forward difference operator for polynomials in one variable. In Sem 2, we do Brzozowski for regular expressions. None of these operators is quite the derivative they learned in school. And then on the test, I give them this thing prop Insertion ABC (List ABC) (RegEx ABC) where -- you can insert b *somewhere* into xs -- to get a string which p likes prove Insertion b xs p by Between as cs where prove xs = as ++ cs prove Likes p (as ++ b : cs) and get them to prove some eerily familiar laws about it...