diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-10-19 22:55:54 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-10-19 22:55:54 -0700 |
| commit | 5a83f112c46196e2a48cb88796751d1a131df122 (patch) | |
| tree | b52d63e4aec99c51fcd7e2790af581a87483f6d3 /Binaries | |
| parent | f8e36475b2abbf642408a8aae0bbce70ab7c86dd (diff) | |
Test cases for co-inductive proofs, and an axiom that makes some of them possible
Diffstat (limited to 'Binaries')
| -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 ---------------------------------------------
|