--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaStackDS.agda	Fri Apr 13 19:47:50 2018 +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₁ where
+  field
+    -- context as set of data segments
+    context : Context
+    stack   : SingleLinkedStack A
+    nextCS  : N.CodeSegment Context Context
+
+open import subtype Meta as M
+