diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
| commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
| tree | 074182834cb406d1304aec4233718564a9c06ba1 /test-suite/output/Notations.out | |
| parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) | |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'test-suite/output/Notations.out')
| -rw-r--r-- | test-suite/output/Notations.out | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 6efd671a..b1558dab 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -70,7 +70,7 @@ FST (0; 1) : Z Nil : forall A : Type, list A -NIL:list nat +NIL : list nat : list nat (false && I 3)%bool /\ I 6 : Prop @@ -78,7 +78,7 @@ NIL:list nat : Z * Z * Z * (Z * Z * Z) [|0 * (1, 2, 3); (4, 5, 6) * false|] : Z * Z * (Z * Z) * (Z * Z) * (Z * bool * (Z * bool) * (Z * bool)) -fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|}:Z +fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|} : Z : (Z -> Z -> Z -> Z) -> Z Init.Nat.add : nat -> nat -> nat |