Agda-2.3.2.2: examples/outdated-and-incorrect/Alonzo/Point.agda

module Point where

open import Nat
open import Bool

-- A record can be seen as a one constructor datatype. In this case:
data Point' : Set where
  mkPoint : (x : Nat)(y : Nat) -> Point'

getX : Point' -> Nat
getX (mkPoint x y) = x

getY : Point' -> Nat
getY (mkPoint x y) = y