Improvements to Nipkow and Klein test cases: Changed imap to map, removed need for Total

1 files changed, 2 insertions, 2 deletions

diff --git a/Test/dafny4/NipkowKlein-chapter3.dfy b/Test/dafny4/NipkowKlein-chapter3.dfy
index 6572359a..ab45f536 100644
--- a/Test/dafny4/NipkowKlein-chapter3.dfy
+++ b/Test/dafny4/NipkowKlein-chapter3.dfy
@@ -18,7 +18,7 @@ function append(xs: List, ys: List): List
 // ----- arithmetic expressions -----

 

 type vname = string  // variable names

-datatype aexp = N(n: int) | V(x: vname) | Plus(0: aexp, 1: aexp)  // arithmetic expressions

+datatype aexp = N(n: int) | V(vname) | Plus(aexp, aexp)  // arithmetic expressions

 

 type val = int

 type state = vname -> val

@@ -133,7 +133,7 @@ lemma AsimpCorrect(a: aexp, s: state)
 

 // ----- boolean expressions -----

 

-datatype bexp = Bc(v: bool) | Not(op: bexp) | And(0: bexp, 1: bexp) | Less(a0: aexp, a1: aexp)

+datatype bexp = Bc(v: bool) | Not(bexp) | And(bexp, bexp) | Less(aexp, aexp)

 

 function bval(b: bexp, s: state): bool

   reads s.reads