sordina

-- Hello Agda Enthusiasts!

-- Let's play with Agda.

-- Firstly, since we're editing demo1A.agda, let's name our module correctly:

module demo1A where -- Load the file with C-c C-l - Like that!

-- Syntax is highlighted by Emacs