explore Big operators as exploration functions in Agda Please use the module Explore/README.agda as a starting point