# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1485850850 -32400
# Node ID ef9730f3db8d6d7f7511d9ddf0e50f5ad4b0e2ec
# Parent  9902994fbd1ae58ddce052ab8dbf8b13b1a80363
Writing agda description ......

diff -r 9902994fbd1a -r ef9730f3db8d paper/src/AgdaImport.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/AgdaImport.agda	Tue Jan 31 17:20:50 2017 +0900
@@ -0,0 +1,6 @@
+import Data.Nat                  -- import module
+import Data.Bool as B            -- renamed module
+import Data.List using (head)    -- import Data.head function
+import Level renaming (suc to S) -- import module with rename suc to S
+import Data.String hiding (_++_) -- import module without _++_
+open import Data.List            -- import and expand Data.List
diff -r 9902994fbd1a -r ef9730f3db8d paper/src/AgdaParameterizedModule.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/AgdaParameterizedModule.agda	Tue Jan 31 17:20:50 2017 +0900
@@ -0,0 +1,6 @@
+module Sort (A : Set) (_<_ : A -> A -> Bool) where
+  sort : List A -> List A
+  sort = ...
+
+open import Sort Nat  Nat._<_  as N
+open import Sort Bool Bool._<_ as B