Test/irondafny0/opened_workaround.dfy


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

// RUN: %dafny /ironDafny /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

module A {

    predicate P() 

    class C
    {
        static method{:axiom} M()
            ensures P();
    } 
}

abstract module B {
    import opened A
}

abstract module C {
    import Bee : B       // Works
}