From 628acc07a07bd5516551dc2caa2c4612f70d2688 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Fri, 23 Oct 2015 18:30:11 -0700
Subject: Introduced new datatype update syntax:  D.(f := E) The old syntax,
 D[f := E], is still supported for a short while, but generates a warning
 about that syntax being deprecated. The new syntax also supports multiple
 updates:  D.(f := E0, g := E1, h := E2)

---
 Test/dafny0/DatatypeUpdateResolution.dfy.expect | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 Test/dafny0/DatatypeUpdateResolution.dfy.expect

(limited to 'Test/dafny0/DatatypeUpdateResolution.dfy.expect')

diff --git a/Test/dafny0/DatatypeUpdateResolution.dfy.expect b/Test/dafny0/DatatypeUpdateResolution.dfy.expect
new file mode 100644
index 00000000..db3e1fe2
--- /dev/null
+++ b/Test/dafny0/DatatypeUpdateResolution.dfy.expect
@@ -0,0 +1,5 @@
+DatatypeUpdateResolution.dfy(12,22): Error: member 'non_destructor' does not exist in datatype 'MyDataType'
+DatatypeUpdateResolution.dfy(13,38): Error: member '40' does not exist in datatype 'MyDataType'
+DatatypeUpdateResolution.dfy(17,61): Error: duplicate update member 'otherbool'
+DatatypeUpdateResolution.dfy(19,23): Error: updated datatype members must belong to the same constructor ('otherbool' belongs to 'MyOtherConstructor' and '42' belongs to 'MyNumericConstructor'
+4 resolution/type errors detected in DatatypeUpdateResolution.dfy
-- 
cgit v1.2.3