diff options
author | Jason Koenig <unknown> | 2012-06-26 17:06:33 -0700 |
---|---|---|
committer | Jason Koenig <unknown> | 2012-06-26 17:06:33 -0700 |
commit | 1fbd28ebc465f94cc783e5d9dcc7c5f206c81e69 (patch) | |
tree | ef703551d73c683958b4503e03abb471928dad26 /Binaries/DafnyPrelude.bpl | |
parent | 4f2f785d121651c62cf0a7da7c7bcaef13ee14b4 (diff) |
Dafny: Implemented abstract modules
Diffstat (limited to 'Binaries/DafnyPrelude.bpl')
-rw-r--r-- | Binaries/DafnyPrelude.bpl | 7 |
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 ----------------------------------------------
// ---------------------------------------------------------------
|