anchor.diff:  
   (is (test/handle-fun-def-1) "let rec f (a: (array int)) (b: int) : int
       requires { true }
  -    ensures  { (c) = (b) }
  +    ensures  { (result) = (b) }
     =
       let b1 : bool = b > 0 in
         match b1 with
  
positive.code: 
  (is (test/letfun-1) "let rec f (a: (array int)) : int
      requires { true }
      ensures  { (c) = (b) }
    =
      let b1 : bool = b > 0 in
  match b1 with
  
negative.code:     requires { (a) = (1) }
      ensures  { let (r1,r2) : (int, int) = result in (r1) = (r2) }
    =
  (a, a)"
    "Tuples are handled in a postcondition"
    :test #'equal-ignore-whitespace))
  
  (finalize)
  