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/Prooftext.gf | |
| parent | 2f68128323462c0488dfc98c09dbc615c1ca9cf1 (diff) | |
overload resolution with value type, for experiment
Diffstat (limited to 'examples/logic/Prooftext.gf')
| -rw-r--r-- | examples/logic/Prooftext.gf | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/examples/logic/Prooftext.gf b/examples/logic/Prooftext.gf index 3a5a61894..4c193740a 100644 --- a/examples/logic/Prooftext.gf +++ b/examples/logic/Prooftext.gf @@ -32,7 +32,7 @@ oper definition : Decls -> Object -> Object -> Section = \decl,a,b -> - appendText decl (mkUtt (mkS (pred b a))) ; + appendText decl (mkText (mkPhr (mkUtt (mkS (pred b a)))) TEmpty) ; theorem : Prop -> Proof -> Section = \prop,prf -> appendText (mkText (mkPhr prop) TEmpty) prf ; @@ -64,17 +64,17 @@ oper = appendText ; cases : Num -> Branching - = \nu -> - mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet nu) case_N)) ; + = \n -> + mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet n) case_N)) ; by : Ref -> Adverb - = \h -> mkAdv by8means_Prep h ; + = \h -> C.mkPConj (mkAdv by8means_Prep h).s ; therefore : Adverb = therefore_PConj ; afortiori : Adverb = C.mkPConj ["a fortiori"] ; hypothesis : Adverb - = mkAdv by8means_Prep (mkNP (mkDet DefArt) hypothesis_N) ; + = C.mkPConj (mkAdv by8means_Prep (mkNP (mkDet DefArt) hypothesis_N)).s ; ref : Label -> Ref = \h -> h ; |