blob: fff6c36a63ca79bb4f2b07c8bdb596abdae1f4f2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
// RUN: %dafny /compile:0 /ironDafny "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
module NativeTypes {
newtype{:nativeType "ushort"} uint16 = i:int | 0 <= i < 0x10000
}
abstract module AbstractModuleA
{
import opened NativeTypes
datatype T = T(i:uint16)
}
abstract module AbstractModuleB
{
import opened A as AbstractModuleA
}
abstract module AbstractModuleC
{
import opened B as AbstractModuleB
}
|
