diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
| commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
| tree | 591e9e512063e34099782e2518573f15ffeac003 /test-suite/output/Notations.out | |
| parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) | |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'test-suite/output/Notations.out')
| -rw-r--r-- | test-suite/output/Notations.out | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 3ab3de45..be4cd4fa 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -14,6 +14,12 @@ forall n : nat, n = 0 : Prop !(0 = 0) : Prop +forall n : nat, #(n = n) + : Prop +forall n n0 : nat, ##(n = n0) + : Prop +forall n n0 : nat, ###(n = n0) + : Prop 3 + 3 : Z 3 + 3 @@ -22,3 +28,21 @@ forall n : nat, n = 0 : list nat (1; 2, 4) : nat * nat * nat +Defining 'ifzero' as keyword +ifzero 3 + : bool +Defining 'pred' as keyword +pred 3 + : nat +fun n : nat => pred n + : nat -> nat +fun n : nat => pred n + : nat -> nat +Defining 'ifn' as keyword +Defining 'is' as keyword +fun x : nat => ifn x is succ n then n else 0 + : nat -> nat +1- + : bool +-4 + : Z |