Merge pull request #1 from adelon/main

Update Fork

5 files changed, 55 insertions, 55 deletions

diff --git a/test/golden/byRef/encoding tasks.golden b/test/golden/byRef/encoding tasks.golden
index 75c9e78..47513ec 100644
--- a/test/golden/byRef/encoding tasks.golden
+++ b/test/golden/byRef/encoding tasks.golden
@@ -1,22 +1,22 @@
-fof(first_proposition,conjecture,fa=fa).
+fof(prop1,conjecture,fa=fa).
 ------------------
-fof(second_proposition,conjecture,fb=fb).
-fof(first_proposition,axiom,![Xa]:Xa=Xa).
+fof(prop2,conjecture,fb=fb).
+fof(prop1,axiom,![Xa]:Xa=Xa).
 ------------------
-fof(third_proposition,conjecture,fc=fc).
-fof(first_proposition,axiom,![Xa]:Xa=Xa).
+fof(prop3,conjecture,fc=fc).
+fof(prop1,axiom,![Xa]:Xa=Xa).
 ------------------
-fof(fourth_proposition,conjecture,![Xd]:Xd=Xd).
-fof(first_proposition,axiom,![Xa]:Xa=Xa).
+fof(prop4,conjecture,![Xd]:Xd=Xd).
+fof(prop1,axiom,![Xa]:Xa=Xa).
 ------------------
-fof(fourth_proposition,conjecture,fe=fe).
-fof(third_proposition,axiom,![Xc]:Xc=Xc).
-fof(second_proposition,axiom,![Xb]:Xb=Xb).
-fof(first_proposition,axiom,![Xa]:Xa=Xa).
-fof(fourth_proposition1,axiom,![Xd]:Xd=Xd).
+fof(prop4,conjecture,fe=fe).
+fof(prop3,axiom,![Xc]:Xc=Xc).
+fof(prop2,axiom,![Xb]:Xb=Xb).
+fof(prop1,axiom,![Xa]:Xa=Xa).
+fof(prop41,axiom,![Xd]:Xd=Xd).
 ------------------
-fof(fifth_proposition,conjecture,ff=ff).
-fof(fourth_proposition,axiom,![Xe]:Xe=Xe).
-fof(third_proposition,axiom,![Xc]:Xc=Xc).
-fof(second_proposition,axiom,![Xb]:Xb=Xb).
-fof(first_proposition,axiom,![Xa]:Xa=Xa).
\ No newline at end of file
+fof(prop5,conjecture,ff=ff).
+fof(prop4,axiom,![Xe]:Xe=Xe).
+fof(prop3,axiom,![Xc]:Xc=Xc).
+fof(prop2,axiom,![Xb]:Xb=Xb).
+fof(prop1,axiom,![Xa]:Xa=Xa).
\ No newline at end of file
diff --git a/test/golden/byRef/generating tasks.golden b/test/golden/byRef/generating tasks.golden
index 3187198..b9fa157 100644
--- a/test/golden/byRef/generating tasks.golden
+++ b/test/golden/byRef/generating tasks.golden
@@ -1,7 +1,7 @@
 [ Task
     { taskDirectness = Direct
     , taskHypotheses = []
-    , taskConjectureLabel = Marker "first_proposition"
+    , taskConjectureLabel = Marker "prop1"
     , taskConjecture = TermSymbol
         ( SymbolPredicate
             ( PredicateRelation
@@ -18,7 +18,7 @@
     { taskDirectness = Direct
     , taskHypotheses =
         [
-            ( Marker "first_proposition"
+            ( Marker "prop1"
             , Quantified Universally
                 ( Scope
                     ( TermSymbol
@@ -40,7 +40,7 @@
                 )
             )
         ]
-    , taskConjectureLabel = Marker "second_proposition"
+    , taskConjectureLabel = Marker "prop2"
     , taskConjecture = TermSymbol
         ( SymbolPredicate
             ( PredicateRelation
@@ -57,7 +57,7 @@
     { taskDirectness = Direct
     , taskHypotheses =
         [
-            ( Marker "first_proposition"
+            ( Marker "prop1"
             , Quantified Universally
                 ( Scope
                     ( TermSymbol
@@ -79,7 +79,7 @@
                 )
             )
         ]
-    , taskConjectureLabel = Marker "third_proposition"
+    , taskConjectureLabel = Marker "prop3"
     , taskConjecture = TermSymbol
         ( SymbolPredicate
             ( PredicateRelation
@@ -96,7 +96,7 @@
     { taskDirectness = Direct
     , taskHypotheses =
         [
-            ( Marker "first_proposition"
+            ( Marker "prop1"
             , Quantified Universally
                 ( Scope
                     ( TermSymbol
@@ -118,7 +118,7 @@
                 )
             )
         ]
-    , taskConjectureLabel = Marker "fourth_proposition"
+    , taskConjectureLabel = Marker "prop4"
     , taskConjecture = Quantified Universally
         ( Scope
             ( TermSymbol
@@ -143,7 +143,7 @@
     { taskDirectness = Direct
     , taskHypotheses =
         [
-            ( Marker "third_proposition"
+            ( Marker "prop3"
             , Quantified Universally
                 ( Scope
                     ( TermSymbol
@@ -165,7 +165,7 @@
                 )
             )
         ,
-            ( Marker "second_proposition"
+            ( Marker "prop2"
             , Quantified Universally
                 ( Scope
                     ( TermSymbol
@@ -187,7 +187,7 @@
                 )
             )
         ,
-            ( Marker "first_proposition"
+            ( Marker "prop1"
             , Quantified Universally
                 ( Scope
                     ( TermSymbol
@@ -209,7 +209,7 @@
                 )
             )
         ,
-            ( Marker "fourth_proposition1"
+            ( Marker "prop41"
             , Quantified Universally
                 ( Scope
                     ( TermSymbol
@@ -231,7 +231,7 @@
                 )
             )
         ]
-    , taskConjectureLabel = Marker "fourth_proposition"
+    , taskConjectureLabel = Marker "prop4"
     , taskConjecture = TermSymbol
         ( SymbolPredicate
             ( PredicateRelation
@@ -248,7 +248,7 @@
     { taskDirectness = Direct
     , taskHypotheses =
         [
-            ( Marker "fourth_proposition"
+            ( Marker "prop4"
             , Quantified Universally
                 ( Scope
                     ( TermSymbol
@@ -270,7 +270,7 @@
                 )
             )
         ,
-            ( Marker "third_proposition"
+            ( Marker "prop3"
             , Quantified Universally
                 ( Scope
                     ( TermSymbol
@@ -292,7 +292,7 @@
                 )
             )
         ,
-            ( Marker "second_proposition"
+            ( Marker "prop2"
             , Quantified Universally
                 ( Scope
                     ( TermSymbol
@@ -314,7 +314,7 @@
                 )
             )
         ,
-            ( Marker "first_proposition"
+            ( Marker "prop1"
             , Quantified Universally
                 ( Scope
                     ( TermSymbol
@@ -336,7 +336,7 @@
                 )
             )
         ]
-    , taskConjectureLabel = Marker "fifth_proposition"
+    , taskConjectureLabel = Marker "prop5"
     , taskConjecture = TermSymbol
         ( SymbolPredicate
             ( PredicateRelation
diff --git a/test/golden/byRef/glossing.golden b/test/golden/byRef/glossing.golden
index e213bc9..cc7281e 100644
--- a/test/golden/byRef/glossing.golden
+++ b/test/golden/byRef/glossing.golden
@@ -5,7 +5,7 @@
         , sourceColumn = Pos 1
         }
     )
-    ( Marker "first_proposition" )
+    ( Marker "prop1" )
     ( Lemma []
         ( TermSymbol
             ( SymbolPredicate
@@ -27,7 +27,7 @@
         , sourceColumn = Pos 1
         }
     )
-    ( Marker "second_proposition" )
+    ( Marker "prop2" )
     ( Lemma []
         ( TermSymbol
             ( SymbolPredicate
@@ -49,7 +49,7 @@
         , sourceColumn = Pos 1
         }
     )
-    ( Marker "third_proposition" )
+    ( Marker "prop3" )
     ( Lemma []
         ( TermSymbol
             ( SymbolPredicate
@@ -73,7 +73,7 @@
     )
     ( Qed
         ( JustificationRef
-            ( Marker "first_proposition" :| [] )
+            ( Marker "prop1" :| [] )
         )
     )
 , BlockLemma
@@ -83,7 +83,7 @@
         , sourceColumn = Pos 1
         }
     )
-    ( Marker "fourth_proposition" )
+    ( Marker "prop4" )
     ( Lemma []
         ( TermSymbol
             ( SymbolPredicate
@@ -127,7 +127,7 @@
             )
         )
         ( JustificationRef
-            ( Marker "first_proposition" :| [] )
+            ( Marker "prop1" :| [] )
         ) ( Qed JustificationEmpty )
     )
 , BlockLemma
@@ -137,7 +137,7 @@
         , sourceColumn = Pos 1
         }
     )
-    ( Marker "fifth_proposition" )
+    ( Marker "prop5" )
     ( Lemma []
         ( TermSymbol
             ( SymbolPredicate
diff --git a/test/golden/byRef/parsing.golden b/test/golden/byRef/parsing.golden
index 2cf91b6..3df8730 100644
--- a/test/golden/byRef/parsing.golden
+++ b/test/golden/byRef/parsing.golden
@@ -5,7 +5,7 @@
         , sourceColumn = Pos 1
         }
     )
-    ( Marker "first_proposition" )
+    ( Marker "prop1" )
     ( Lemma []
         ( StmtFormula
             ( FormulaChain
@@ -30,7 +30,7 @@
         , sourceColumn = Pos 1
         }
     )
-    ( Marker "second_proposition" )
+    ( Marker "prop2" )
     ( Lemma []
         ( StmtFormula
             ( FormulaChain
@@ -55,7 +55,7 @@
         , sourceColumn = Pos 1
         }
     )
-    ( Marker "third_proposition" )
+    ( Marker "prop3" )
     ( Lemma []
         ( StmtFormula
             ( FormulaChain
@@ -82,7 +82,7 @@
     )
     ( Qed
         ( JustificationRef
-            ( Marker "first_proposition" :| [] )
+            ( Marker "prop1" :| [] )
         )
     )
 , BlockLemma
@@ -92,7 +92,7 @@
         , sourceColumn = Pos 1
         }
     )
-    ( Marker "fourth_proposition" )
+    ( Marker "prop4" )
     ( Lemma []
         ( StmtFormula
             ( FormulaChain
@@ -137,7 +137,7 @@
             )
         )
         ( JustificationRef
-            ( Marker "first_proposition" :| [] )
+            ( Marker "prop1" :| [] )
         ) ( Qed JustificationEmpty )
     )
 , BlockLemma
@@ -147,7 +147,7 @@
         , sourceColumn = Pos 1
         }
     )
-    ( Marker "fifth_proposition" )
+    ( Marker "prop5" )
     ( Lemma []
         ( StmtFormula
             ( FormulaChain
diff --git a/test/golden/byRef/tokenizing.golden b/test/golden/byRef/tokenizing.golden
index 2ae8ea6..aed896f 100644
--- a/test/golden/byRef/tokenizing.golden
+++ b/test/golden/byRef/tokenizing.golden
@@ -1,5 +1,5 @@
 [ BeginEnv "proposition"
-, Label "first_proposition"
+, Label "prop1"
 , BeginEnv "math"
 , Variable "a"
 , Symbol "="
@@ -8,7 +8,7 @@
 , Symbol "."
 , EndEnv "proposition"
 , BeginEnv "proposition"
-, Label "second_proposition"
+, Label "prop2"
 , BeginEnv "math"
 , Variable "b"
 , Symbol "="
@@ -17,7 +17,7 @@
 , Symbol "."
 , EndEnv "proposition"
 , BeginEnv "proposition"
-, Label "third_proposition"
+, Label "prop3"
 , BeginEnv "math"
 , Variable "c"
 , Symbol "="
@@ -29,11 +29,11 @@
 , Word "follows"
 , Word "by"
 , Ref
-    ( "first_proposition" :| [] )
+    ( "prop1" :| [] )
 , Symbol "."
 , EndEnv "proof"
 , BeginEnv "proposition"
-, Label "fourth_proposition"
+, Label "prop4"
 , BeginEnv "math"
 , Variable "e"
 , Symbol "="
@@ -56,11 +56,11 @@
 , EndEnv "math"
 , Word "by"
 , Ref
-    ( "first_proposition" :| [] )
+    ( "prop1" :| [] )
 , Symbol "."
 , EndEnv "proof"
 , BeginEnv "proposition"
-, Label "fifth_proposition"
+, Label "prop5"
 , BeginEnv "math"
 , Variable "f"
 , Symbol "="