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/ArithmEng.gf | |
| parent | 2f68128323462c0488dfc98c09dbc615c1ca9cf1 (diff) | |
overload resolution with value type, for experiment
Diffstat (limited to 'examples/logic/ArithmEng.gf')
| -rw-r--r-- | examples/logic/ArithmEng.gf | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/examples/logic/ArithmEng.gf b/examples/logic/ArithmEng.gf index 05526b365..1ab4c2abd 100644 --- a/examples/logic/ArithmEng.gf +++ b/examples/logic/ArithmEng.gf @@ -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 = |