GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-04-20 10:19:32 -06:00
Code Issues Packages Projects Releases Wiki Activity

overload resolution with value type, for experiment

Browse Source
This commit is contained in:
aarne
2006-12-19 23:34:36 +00:00
parent 339aeb8bf6
commit 7bba9d1491
5 changed files with 46 additions and 28 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
examples/logic/ArithmEng.gf
View File

@@ -29,15 +29,15 @@ lin
evax1 =
proof (by (ref (mkLabel ["the first axiom of evenness ,"])))
(mkS (pred (regA "even") (UsePN (regPN "zero")))) ;
(mkS (predA (regA "even") (UsePN (regPN "zero")))) ;
evax2 n c =
appendText c
(proof (by (ref (mkLabel ["the second axiom of evenness ,"])))
(mkS (pred (regA "odd") (appN2 (regN2 "successor") n)))) ;
(mkS (predA (regA "odd") (appN2 (regN2 "successor") n)))) ;
evax3 n c =
appendText c
(proof (by (ref (mkLabel ["the third axiom of evenness ,"])))
(mkS (pred (regA "even") (appN2 (regN2 "successor") n)))) ;
(mkS (predA (regA "even") (appN2 (regN2 "successor") n)))) ;
eqax1 =

14
examples/logic/LogicI.gf
View File

@@ -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 =

10
examples/logic/Prooftext.gf
View File

@@ -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 ;