echo< echo> hello
echo< echo> my
echo< echo> name
echo< echo> is
echo< echo> Agda
echo<