diff options
| author | aarne <aarne@cs.chalmers.se> | 2006-11-27 21:03:15 +0000 |
|---|---|---|
| committer | aarne <aarne@cs.chalmers.se> | 2006-11-27 21:03:15 +0000 |
| commit | 0c5f2c12880d339e51e5133c61216f233d5a9a7b (patch) | |
| tree | 6058960ad196dd410184ccebf73ba4473830ef11 /examples/logic/LogicI.gf | |
| parent | 8cd9a329fa6d41849df4b7e8c2f19b34884cb547 (diff) | |
more in ArithmEng
Diffstat (limited to 'examples/logic/LogicI.gf')
| -rw-r--r-- | examples/logic/LogicI.gf | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/examples/logic/LogicI.gf b/examples/logic/LogicI.gf index 61d948607..09ffe661d 100644 --- a/examples/logic/LogicI.gf +++ b/examples/logic/LogicI.gf @@ -4,8 +4,7 @@ incomplete concrete LogicI of Logic = Prooftext, Grammar, Constructors, - Combinators, - ParamX --- + Combinators in { lincat @@ -19,10 +18,12 @@ lincat lin ThmWithProof = theorem ; + Conj A B = coord and_Conj A B ; Disj A B = coord or_Conj A B ; Impl A B = coord ifthen_DConj A B ; - Abs = mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet IndefArt) contradiction_N)) ; + Abs = + mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet IndefArt) contradiction_N)) ; Univ A B = AdvS @@ -45,13 +46,14 @@ lin (proof therefore C)) ; ImplI A B b = - proof (assumption A) (appendText b (proof therefore (coord ifthen_DConj A B))) ; + proof + (assumption A) + (appendText b (proof therefore (coord ifthen_DConj A B))) ; Hypoth A h = proof hypothesis A ; ---- this should not be here, but is needed for variables lindef - Elem s = {s = \\_ => s ; a = {n = Sg ; p = P3} ; lock_NP = <>} ; + Elem = defNP ; -}
\ No newline at end of file +} |