From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 test-suite/output/Notations.out | 37 ++++++++++++++++++++++++++++++++++++-
 1 file changed, 36 insertions(+), 1 deletion(-)

(limited to 'test-suite/output/Notations.out')

diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 42858304..924030ba 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -1,7 +1,7 @@
 true ? 0; 1
      : nat
 if true as x return (x ? nat; bool) then 0 else true
-     : true ? nat; bool
+     : nat
 Defining 'proj1' as keyword
 fun e : nat * nat => proj1 e
      : nat * nat -> nat
@@ -46,6 +46,10 @@ fun x : nat => ifn x is succ n then n else 0
      : bool
 -4
      : Z
+SUM (nat * nat) nat
+     : Set
+FST (0; 1)
+     : Z
 Nil
      : forall A : Type, list A
 NIL:list nat
@@ -57,3 +61,34 @@ Defining 'I' as keyword
      : Z * Z * Z * (Z * Z * Z)
 fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|}:Z
      : (Z -> Z -> Z -> Z) -> Z
+plus
+     : nat -> nat -> nat
+S
+     : nat -> nat
+mult
+     : nat -> nat -> nat
+le
+     : nat -> nat -> Prop
+plus
+     : nat -> nat -> nat
+succ
+     : nat -> nat
+mult
+     : nat -> nat -> nat
+le
+     : nat -> nat -> Prop
+fun x : option Z => match x with
+                    | SOME x0 => x0
+                    | NONE => 0
+                    end
+     : option Z -> Z
+fun x : option Z => match x with
+                    | SOME2 x0 => x0
+                    | NONE2 => 0
+                    end
+     : option Z -> Z
+fun x : option Z => match x with
+                    | SOME3 x0 => x0
+                    | NONE3 => 0
+                    end
+     : option Z -> Z
-- 
cgit v1.2.3