From 474402019659b954371e46891f0e6ac8679dd574 Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Tue, 26 Jun 2012 17:06:33 -0700
Subject: Dafny: Implemented abstract modules

---
 Binaries/DafnyPrelude.bpl | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'Binaries')

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 ----------------------------------------------
 // ---------------------------------------------------------------
-- 
cgit v1.2.3