diff options
| author | aarne <aarne@cs.chalmers.se> | 2006-11-26 17:14:20 +0000 |
|---|---|---|
| committer | aarne <aarne@cs.chalmers.se> | 2006-11-26 17:14:20 +0000 |
| commit | c75688651e95d1fe69175ca3e4859e6d753b2b8c (patch) | |
| tree | e4f0163d12a2cdfd078daa1b8564a916db411863 /examples/logic/TheoryI.gf | |
| parent | 13531a66a3cd2c65eeac8ce12b283528744a7adf (diff) | |
a logic library; fix in make mathematical
Diffstat (limited to 'examples/logic/TheoryI.gf')
| -rw-r--r-- | examples/logic/TheoryI.gf | 56 |
1 files changed, 56 insertions, 0 deletions
diff --git a/examples/logic/TheoryI.gf b/examples/logic/TheoryI.gf new file mode 100644 index 000000000..9ab457536 --- /dev/null +++ b/examples/logic/TheoryI.gf @@ -0,0 +1,56 @@ +incomplete concrete TheoryI of Theory = + open + LexTheory, + Grammar, + Symbolic, + Symbol, + Combinators, + Constructors, + (C=ConstructX), + Prelude + in { + +lincat + Chapter = Text ; + Jment = Text ; + Decl = Text ; + Prop = S ; + Branch = S ; + Proof = Text ; + [Proof] = Text ; + Typ = CN ; + Obj = NP ; + Label = NP ; + Adverb = PConj ; + Ref = NP ; + [Ref] = [NP] ; + Number = Num ; + +lin + Chap title jments = + appendText (mkText (mkPhr (mkUtt title)) TEmpty) jments ; + + JDefObj decl a b = + appendText decl (mkUtt (mkS (pred b a))) ; + + DProp p = + mkText (mkPhr (mkUtt (mkImp (mkVP assume_VS p)))) TEmpty ; + DTyp a ty = --- x pro a: refresh bug + mkText (mkPhr (mkUtt (mkImp (mkVP assume_VS (mkS (pred ty a)))))) TEmpty ; + + PProp p = mkText (mkPhr p) TEmpty ; + PAdvProp a p = mkText (mkPhr a (mkUtt p) NoVoc) TEmpty ; + PDecl d = d ; + PBranch b ps = mkText (mkPhr b) ps ; + + BCases n = + mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet (mkNum n2)) case_N)) ; + + ARef h = mkAdv by8means_Prep h ; + AHence = therefore_PConj ; + AAFort = C.mkPConj ["a fortiori"] ; + + RLabel h = h ; + RMany rs = mkNP and_Conj rs ; + +} |