packages feed

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

{-# OPTIONS -fglasgow-exts #-}

-- Generated by Alonzo

module Point where
import RTS
import qualified RTP
import qualified Nat
import qualified Bool
name1 = "Point'"
 
data T1 a b = C4 a b
d1 = ()
name4 = "mkPoint"
name5 = "getX"
d5 = d5_1
  where d5_1 (Point.C4 v0 _) = cast v0
name8 = "getY"
d8 = d8_1
  where d8_1 (Point.C4 _ v0) = cast v0