changes related to paper

examples.gfs

 i gf/MNlpEng.gf
-parse "a positive integer $ mi( n ) $ is called prime iff there is no integer $ mrow( mn( 1 ) mo( < ) mi( m ) mo( < ) mi( n ) ) $ such that $ mrow( mi( m ) mo( | ) mi( n ) ) $"
+i gf/MNlpLog.gf
+parse "a positive integer $ mi( n ) $ is called prime iff there is no integer $ mrow( mn( 1 ) mo( < ) mi( m ) mo( < ) mi( n ) ) $ such that $ mrow( mi( m ) mo( | ) mi( n ) ) $" | l -lang=Log
 parse "a set is called empty iff it is the empty set"
 parse "an alphabet $ mi( A ) $ is a finite set"

gf/NGrammar.gf

@@ -27,6 +27,7 @@ abstract NGrammar = MCats, Grammar, Extra, ExtraEngAbs ** {
         def_mobj_is_mobj : MObj -> Identifier -> MObj -> Definition; -- "an alphabet $A$ is a finite set
 
         let_id_be_a_mobj : Identifier -> MObj -> Declaration;
+        let_then_stmt : Identifier -> MObj -> StatementFin -> StatementFin;
 
         utter_statement : StatementFin -> Utterance;          -- essentially identity
         utter_definition : Definition -> Utterance;           -- essentially identity

gf/NGrammarEng.gf

@@ -34,14 +34,18 @@ concrete NGrammarEng of NGrammar = MCatsEng, GrammarEng, ExtraEng ** open Syntax
         iff_definition defi condition = lin S { s = defi.s ++ "iff" ++ condition.s.s }; -- better solution for this?
 --        def_defmobj_defmobj a b = mkCl a b;
         def_mobj_is_mobj definiendum id definiens =
-                mkS (mkCl (DetCN aSg_Det (mobjToCN definiendum id)) (mobjToCN definiens))  -- a unitary quasigroup is a loop
-                | mkS (mkCl (DetCN aSg_Det (mobjToCN definiendum id))                      -- a unitary quasigroup is called a loop
-                            (PastPartAP (mkVPSlash call_V3 (DetCN aSg_Det (mobjToCN definiens)))));
+                mkS (mkCl (DetCN aSg_Det (mobjToCN definiens id)) (mobjToCN definiendum))  -- a unitary quasigroup is a loop
+                | mkS (mkCl (DetCN aSg_Det (mobjToCN definiens id))                      -- a unitary quasigroup is called a loop
+                            (PastPartAP (mkVPSlash call_V3 (DetCN aSg_Det (mobjToCN definiendum)))));
 --            mkS (mkCl (DetCN {- mkNP is for some reason ambiguous -}
 --                        aSg_Det (appo_mobj definiendum representative)) definiens);
 
 
-        let_id_be_a_mobj id obj = ImpP3 (identifierToNP id) (mkVP (mobjToCN obj));
+--        let_id_be_a_mobj id obj = ImpP3 (identifierToNP id) (mkVP (mobjToCN obj));
+--        let_then_stmt id obj stmt = {
+--            s = mkS (mkConj "then") { s = (ImpP3 (identifierToNP id) (mkVP (mobjToCN obj))).s } stmt.s;
+--            rs = mkRS (mkConj "then") { s = (ImpP3 (identifierToNP id) (mkVP (mobjToCN obj))).s } stmt.rs;
+--            };
 
         utter_statement s = mkUtt s.s;
         utter_declaration s = mkUtt s;

gf/NGrammarLog.gf

@@ -26,8 +26,8 @@ concrete NGrammarLog of NGrammar = MCatsLog ** {
             pref = defi.pref ++ "⇔" ++ condition;
             postf = defi.postf;
         };
-        def_mobj_is_mobj definiendum definiens = {
-            pref = "∀" ++ "x0" ++ "." ++ lwrap(definiens) ++ "x0" ++ "⇒" ++ "(" ++ lwrap(definiendum) ++ "x0";
+        def_mobj_is_mobj definiendum id definiens = {
+            pref = "∀" ++ "x0" ++ "." ++ (lwrap(definiens) ++ id.core ++ and_formula(id)) ++ "⇒" ++ "(" ++ lwrap(definiendum) ++ id.core;
             postf = ")";
         };