Merge pull request #37 from HalflingHelper/all_elim_fix

Remove Marks Fix

abstract_syntax.py

@@ -1136,7 +1136,7 @@ def copy(self):
     #             self.subject.copy())
 
   def __str__(self):
-    return '{' + str(self.subject) + '}'
+    return '#' + str(self.subject) + '#'
 
   def reduce(self, env):
     subject_red = self.subject.reduce(env)

proof_checker.py

@@ -436,7 +436,7 @@ def check_proof(proof, env):
           error(loc, "\nhave " + label + ':\n\t' + str(proved_formula))
         case _:
           check_proof_of(reason, new_frm, env)
-          body_env = env.declare_local_proof_var(loc, label, new_frm)
+          body_env = env.declare_local_proof_var(loc, label, remove_mark(new_frm))
           ret = check_proof(rest, body_env)
 
     case PAnnot(loc, claim, reason):
@@ -1070,7 +1070,7 @@ def check_proof_of(proof, formula, env):
           error(loc, "\nhave " + base_name(label) + ':\n\t' + str(proved_formula))
         case _:
           check_proof_of(reason, new_frm, env)
-          body_env = env.declare_local_proof_var(loc, label, new_frm)
+          body_env = env.declare_local_proof_var(loc, label, remove_mark(new_frm))
           check_proof_of(rest, formula, body_env)
 
     case PAnnot(loc, claim, reason):

test/should-error/have_remove_marks.pf

@@ -0,0 +1,12 @@
+import List
+import Nat
+
+theorem blah : all x : Nat.
+  length(node(x, empty)) = 1
+proof
+  arbitrary x : Nat
+  have step : length(@empty<Nat>) + #length(@empty<Nat>)#
+    = length(@empty<Nat>) + 0
+    by definition length
+  ?
+end

test/should-error/have_remove_marks.pf.err

@@ -0,0 +1,11 @@
+./test/should-error/have_remove_marks.pf:11.3-11.4: incomplete proof
+Goal:
+	length([x]) = 1
+Advice:
+	To prove this equality, one of these statements might help:
+		definition
+		rewrite
+		equations
+
+Givens:
+	step: length([]) + length([]) = length([]) + 0