module AgdaBasics where