From 38f10721c27f2b8fa68dcb54b5d2423c8d06981f Mon Sep 17 00:00:00 2001
From: hondet <gabrielhondet@gmail.com>
Date: Tue, 1 Dec 2020 08:29:20 +0100
Subject: [PATCH] commenting incomplete spec

---
 paper/stack.lp | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/paper/stack.lp b/paper/stack.lp
index 04d1544..8e7c779 100644
--- a/paper/stack.lp
+++ b/paper/stack.lp
@@ -23,7 +23,8 @@ rule top (push $x _) ↪ $x
 symbol pop_push (x: El t) (s: El stack): Prf ((pop (push x s)) = s)
 symbol top_push (x: El t) (s: El stack): Prf ((top (push x s)) = x)
 
-theorem pop2push2 (x y: El t) (s: El stack)
-      : Prf (pop (pair (pop (push x (fst (push y s)))) _) = s)
-proof
-qed
+// The following theorem has unsolved meta variables
+// theorem pop2push2 (x y: El t) (s: El stack)
+//       : Prf (pop (pair (pop (push x (fst (push y s)))) _) = s)
+// proof
+// qed
-- 
GitLab