Dafny: Implemented abstract modules

1 files changed, 7 insertions, 0 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index fef8fe1f..53d0b471 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -500,6 +500,13 @@ axiom (forall f: Field BoxType, i: int :: { MultiIndexField(f,i) }
 

 function DeclType<T>(Field T): ClassName;

 

+type NameFamily;

+function DeclName<T>(Field T): NameFamily;

+function FieldOfDecl<alpha>(ClassName, NameFamily): Field alpha;

+axiom (forall<T> cl : ClassName, nm: NameFamily :: 

+   {FieldOfDecl(cl, nm): Field T}

+   DeclType(FieldOfDecl(cl, nm): Field T) == cl && DeclName(FieldOfDecl(cl, nm): Field T) == nm);

+

 // ---------------------------------------------------------------

 // -- Allocatedness ----------------------------------------------

 // ---------------------------------------------------------------