blob: 638a897ca68f18f9a3ef7db3d991082550c987e0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
// RUN: %dafny /compile:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
module M1
{
predicate X(i:int)
}
module M2
{
import opened M1
predicate P(i:int) requires X(i) { true } // ok
predicate{:opaque} O(i:int) requires X(i) { true } // resolution/type error: X does not exist
}
|
