diff options
| author | aarne <aarne@cs.chalmers.se> | 2006-12-19 23:34:36 +0000 |
|---|---|---|
| committer | aarne <aarne@cs.chalmers.se> | 2006-12-19 23:34:36 +0000 |
| commit | 0bf909b0fd50a29f9d52a82f50c12af0c6abbc9e (patch) | |
| tree | 9eb74ff00aad09321cec312d4ef0662937342dcd /examples/logic/LogicI.gf | |
| parent | 2f68128323462c0488dfc98c09dbc615c1ca9cf1 (diff) | |
overload resolution with value type, for experiment
Diffstat (limited to 'examples/logic/LogicI.gf')
| -rw-r--r-- | examples/logic/LogicI.gf | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/examples/logic/LogicI.gf b/examples/logic/LogicI.gf index f8eaf6aa2..1f9b08e41 100644 --- a/examples/logic/LogicI.gf +++ b/examples/logic/LogicI.gf @@ -18,9 +18,9 @@ lincat lin ThmWithProof = theorem ; - Conj A = coord and_Conj A ; - Disj A B = coord or_Conj A B ; - Impl A B = coord ifthen_DConj A B ; + Conj = coord and_Conj ; + Disj = coord or_Conj ; + Impl = coord ifthen_DConj ; Abs = mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet IndefArt) contradiction_N)) ; @@ -28,21 +28,21 @@ lin Univ A B = AdvS (mkAdv for_Prep (mkNP all_Predet - (mkNP (mkDet (PlQuant IndefArt)) (mkCN A (symb B.$0))))) + (mkNP (mkDet (PlQuant IndefArt) NoNum NoOrd) (mkCN A (symb B.$0))))) B ; DisjIl A B a = proof a (proof afortiori (coord or_Conj A B)) ; DisjIr A B b = proof b (proof afortiori (coord or_Conj A B)) ; - DisjE A B C c b1 b2 = + DisjE A B C c d e = appendText c (appendText (appendText (cases (mkNum n2)) (proofs - (appendText (assumption A) b1) - (appendText (assumption B) b2))) + (appendText (assumption A) d) + (appendText (assumption B) e))) (proof therefore C)) ; ImplI A B b = |