gallais · March 3, 2017 16:08
diff --git a/Compiled-252.agda b/Compiled-252.agda
 module Compiled-252 where

 data U : Set where
  z : U
  s : U → U

 {-# IMPORT Compiled.URaw #-}
 {-# COMPILED_DATA U Compiled.URaw.U Compiled.URaw.Z Compiled.URaw.S #-}
diff --git a/Compiled-253.agda b/Compiled-253.agda
 module Compiled-253 where

 data U : Set where
  z : U
  s : U → U

 {-# FOREIGN GHC import qualified Compiled.URaw #-}
 {-# COMPILE GHC U = data Compiled.URaw.U (Compiled.URaw.Z | Compiled.URaw.S) #-}
diff --git a/Compiled.agda b/Compiled.agda
 module Compiled where

 -- open import Compiled-252
 open import Compiled-253

 pred : U → U
 pred z     = z
 pred (s t) = t
diff --git a/Compiled.URaw.hs b/Compiled.URaw.hs
 module Compiled.URaw where

 data U = Z | S U
	module Compiled-252 where

	data U : Set where
	z : U
	s : U → U

	{-# IMPORT Compiled.URaw #-}
	{-# COMPILED_DATA U Compiled.URaw.U Compiled.URaw.Z Compiled.URaw.S #-}
	module Compiled-253 where

	data U : Set where
	z : U
	s : U → U

	{-# FOREIGN GHC import qualified Compiled.URaw #-}
	{-# COMPILE GHC U = data Compiled.URaw.U (Compiled.URaw.Z \| Compiled.URaw.S) #-}