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

Fristi

{-# LANGUAGE TypeFamilies #-}

import Data.Function (on)
import Control.Applicative

data EventData e = EventData {
    eventId :: Int,
    body :: Event e
}