blob: ffabbb9218dbd847cb74de9a26f4d8a884f558c4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
// RUN: %dafny /compile:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
datatype PartRealPartGhost = PartRealPartGhost(x:int, ghost y:int)
method UpdateField()
{
var v := PartRealPartGhost(3, 4);
ghost var g := 5;
v := v[y := g];
v := v.(y := g);
}
|
