diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-10-12 18:57:50 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-10-12 18:57:50 -0700 |
| commit | e889485e915a28aa499d19bc194bc731c89033b9 (patch) | |
| tree | d09361dddc2723a93e6e43680bcfcfedacd22b13 /Binaries/DafnyPrelude.bpl | |
| parent | 7007ceb3745e66b251578cee604c1e6249d4a8c3 (diff) | |
Change the encoding of proof certificates to make the two levels explicit
Restrict what conclusions comethods are allowed to have
Diffstat (limited to 'Binaries/DafnyPrelude.bpl')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index c23e8a7e..8ca70bac 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -471,7 +471,8 @@ function DatatypeCtorId(DatatypeType): DtCtorId; function DtRank(DatatypeType): int;
-function CoDatatypeCertificate#Equal(DatatypeType, DatatypeType): bool;
+function CoDatatypeCertificate#Equal0(DatatypeType, DatatypeType): bool;
+function CoDatatypeCertificate#Equal1(DatatypeType, DatatypeType): bool;
// ---------------------------------------------------------------
// -- Axiom contexts ---------------------------------------------
|