view paper/src/AgdaRecordProj.agda @ 109:f6d00a13f923

Add ()
author atton
date Mon, 13 Feb 2017 14:11:30 +0900
parents 10a550bf7e4a
children
line wrap: on
line source

getX : Point -> Nat
getX p = Point.x p

getY : Point -> Nat
getY record { x = a ; y = b} = b

xPlus5 : Point -> Point
xPlus5 p = record p { x = (Point.x p) + 5}