diff options
| author | aarne <aarne@cs.chalmers.se> | 2006-12-21 09:25:02 +0000 |
|---|---|---|
| committer | aarne <aarne@cs.chalmers.se> | 2006-12-21 09:25:02 +0000 |
| commit | fd90fe0791961982570835582dc900627ee62cd5 (patch) | |
| tree | 2c86c977b6c1dd095726673c1c98e6e12411fad8 /examples/logic/ArithmEng.gf | |
| parent | 15fd1d590a70be3af1b4e0a6488ebba795922342 (diff) | |
overload rules and their documentation
Diffstat (limited to 'examples/logic/ArithmEng.gf')
| -rw-r--r-- | examples/logic/ArithmEng.gf | 8 |
1 files changed, 4 insertions, 4 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 = |