Skip to content

Commit

Permalink
fix
Browse files Browse the repository at this point in the history
  • Loading branch information
lucasmcdonald3 committed Dec 12, 2023
1 parent e3b0092 commit d007442
Show file tree
Hide file tree
Showing 3 changed files with 7 additions and 1 deletion.
2 changes: 2 additions & 0 deletions TestModels/ExternV2/src/IndexDotNamespaced.dfy
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0
include "Index.dfy"

module {:extern "simple.dafnyexternv2.internaldafny"} UnderscoreNamespacedSimpleExternV2 replaces SimpleExternV2 {}
2 changes: 2 additions & 0 deletions TestModels/ExternV2/src/IndexUnderscoreNamespaced.dfy
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0
include "Index.dfy"

// TODO: Python will use this syntax.
Expand Down
4 changes: 3 additions & 1 deletion TestModels/ExternV2/test/WrappedTestUnderscoreNamespaced.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -5,4 +5,6 @@ include "SimpleExternV2ImplTest.dfy"
include "WrappedSimpleExternV2ImplTest.dfy"

// TOOD: Python will use this syntax.
module {:extern "simple_dafnyexternv2_internaldafny_wrapped"} UnderscoreNamespacedWrappedSimpleExternV2Service replaces WrappedSimpleExternV2Service {}
module {:extern "simple_dafnyexternv2_internaldafny_wrapped"} UnderscoreNamespacedWrappedSimpleExternV2Service replaces WrappedSimpleExternV2Service {

}

0 comments on commit d007442

Please sign in to comment.