--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/prepaper/src/AgdaStackDS.agda.replaced	Tue Dec 08 19:06:49 2020 +0900
@@ -0,0 +1,17 @@
+record Context : Set where
+  field
+    -- fields for stack
+    element : Maybe A
+
+
+open import subtype Context as N
+
+record Meta  : Set@$\_{1}$@ where
+  field
+    -- context as set of data segments
+    context : Context
+    stack   : SingleLinkedStack A
+    nextCS  : N.CodeSegment Context Context
+
+open import subtype Meta as M
+