diff options
Diffstat (limited to 'Binaries/DafnyPrelude.bpl')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index a605ba87..4118397c 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -482,6 +482,7 @@ function DtRank(DatatypeType): int; function CoDatatypeCertificate#Equal0(DatatypeType, DatatypeType): bool;
function CoDatatypeCertificate#Equal1(DatatypeType, DatatypeType): bool;
+axiom (forall d, e: DatatypeType :: d == e ==> CoDatatypeCertificate#Equal0(d, e));
// ---------------------------------------------------------------
// -- Axiom contexts ---------------------------------------------
|