- forward declaration of records - fixes to projections - drop record accessors (use projections instead) - changes to names to disambiguate
19 lines
219 B
Agda
19 lines
219 B
Agda
module ForwardRecord
|
|
|
|
import Prelude
|
|
|
|
record Point where
|
|
x : Int
|
|
y : Int
|
|
|
|
instance Show Point
|
|
|
|
|
|
instance Show Point where
|
|
show pt = show pt.x ++ "," ++ show pt.y
|
|
|
|
|
|
main : IO Unit
|
|
main = do
|
|
printLn $ MkPoint 1 2
|