diff options
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/logic/ArithmEng.gf | 8 | ||||
| -rw-r--r-- | examples/logic/LogicI.gf | 2 | ||||
| -rw-r--r-- | examples/logic/Prooftext.gf | 2 |
3 files changed, 6 insertions, 6 deletions
diff --git a/examples/logic/ArithmEng.gf b/examples/logic/ArithmEng.gf index 1ab4c2abd..21b68dd03 100644 --- a/examples/logic/ArithmEng.gf +++ b/examples/logic/ArithmEng.gf @@ -24,8 +24,8 @@ lin one = UsePN (regPN "one") ; two = UsePN (regPN "two") ; - sum = appColl (regN2 "sum") ; - prod = appColl (regN2 "product") ; + sum = app (regN2 "sum") ; + prod = app (regN2 "product") ; evax1 = proof (by (ref (mkLabel ["the first axiom of evenness ,"]))) @@ -42,14 +42,14 @@ lin eqax1 = proof (by (ref (mkLabel ["the first axiom of equality ,"]))) - (mkS (predA2 (mkA2 (regA "equal") (mkPrep "to")) + (mkS (pred (mkA2 (regA "equal") (mkPrep "to")) (UsePN (regPN "zero")) (UsePN (regPN "zero")))) ; eqax2 m n c = appendText c (proof (by (ref (mkLabel ["the second axiom of equality ,"]))) - (mkS (predA2 (mkA2 (regA "equal") (mkPrep "to")) + (mkS (pred (mkA2 (regA "equal") (mkPrep "to")) (appN2 (regN2 "successor") m) (appN2 (regN2 "successor") n)))) ; IndNat C d e = {s = diff --git a/examples/logic/LogicI.gf b/examples/logic/LogicI.gf index 1f9b08e41..3598022ac 100644 --- a/examples/logic/LogicI.gf +++ b/examples/logic/LogicI.gf @@ -28,7 +28,7 @@ lin Univ A B = AdvS (mkAdv for_Prep (mkNP all_Predet - (mkNP (mkDet (PlQuant IndefArt) NoNum NoOrd) (mkCN A (symb B.$0))))) + (mkNP (mkDet (PlQuant IndefArt)) (mkCN A (symb B.$0))))) B ; DisjIl A B a = proof a (proof afortiori (coord or_Conj A B)) ; diff --git a/examples/logic/Prooftext.gf b/examples/logic/Prooftext.gf index 4c193740a..1833d6308 100644 --- a/examples/logic/Prooftext.gf +++ b/examples/logic/Prooftext.gf @@ -55,7 +55,7 @@ oper proof : Decl -> Proof = \d -> d ; proof : Proof -> Proof -> Proof - = \p,q -> appendText p q ; + = appendText ; proof : Branching -> Proofs -> Proof = \b,ps -> mkText (mkPhr b) ps } ; |