Hi, I noticed today that there is a web service called "Try It Online" that allows one to try out code written in many languages, including Agda: https://tio.run/#agda Apparently Agda is classified as "practical" rather than "recreational". :) -- /NAD