anchor.diff:          ///         to make sure.
           ///     </para>
           /// </summary>
  -        | NoSuchView of name : string
  +        | NoSuchView of func : DFunc
           /// <summary>
           ///     A view lookup failed during downclosure checking.
           ///
  
positive.code: 
          (* This is needed for base downclosure checking.
             If it doesn't exist, then we don't do those checks. *)
          let empDefn =
              definer
              |> ViewDefiner.toSeq
              |> Seq.tryFind (fst >> List.isEmpty)
              |> Option.bind snd
  
          let checkEach def definer =
              ok def >>= checkDef empDefn vprotos >>= (fun _ -> ok definer)
  
          definer |> ViewDefiner.toSeq |> seqBind checkEach definer
  
  /// Splits an iterated GFunc into a pair of guard and iterated func.
  let iterGFuncTuple
  
negative.code:            The definition of emp can only mention global variables, so it does
             not need to be freshened. *)
          let check = mkImplies empDefn baseDefn
          bind
              (fun baseHolds ->
                  if baseHolds
                  then ok (func, defn)
                  else fail (BaseDownclosureError ([func], defn, empDefn)))
              (runDownclosureCheck check)
  
      /// <summary>
      ///     Checks the inductive downclosure property.
      ///     <para>
      ///         This states that, for all iterated views <c>A(x)[n]</c>,
      ///         for all positive <c>n</c>, <c>D(A(x)[n+1]) => D(A(x)[n])</c>:
      ///         iterated view definitions must be monotonic over the iterator.
      ///         This, coupled with base downclosure, allows us to consider only
      ///         the highest iterator of an iterated func during reification,
      ///         instead of needing to take all funcs with an iterator less than
      ///         or equal to it.
      ///     </para>
      /// </summary>
      /// <param name="iterator">The iterator variable, <c>n</c>.</param>
      /// <param name="func">The iterated func to check, <c>A(x)[n]</c>.</param>
      /// <param name="defn">The definition to check, <c>D(A(x)[n])</c>.</param>
      /// <returns>
      ///     The original definition if inductive downclosure holds; an error
      ///     otherwise.
      /// </returns>
      let checkInductiveDownclosure (iterator : Var)
        (func : IteratedDFunc)
        (defn : BoolExpr<Sym<Var>>)
        : Result<IteratedDFunc * BoolExpr<Sym<Var>>, Error> =
          (* To do the inductive downclosure, we need to replace all instances of
             the iterator in the definition with (iterator + 1) in one version. *)
          let increment v = mkAdd2 (AVar (Reg v)) (AInt 1L)
          let succDefn = mapOverIteratorUses increment iterator defn
  
          (* Inductive downclosure for a view V[n](x):
               (0 <= n) => (D(V[n+1](x)) => D(V[n](x)))
             That is, the definition of V when the iterator is n+1 implies the
             definition of V when the iterator is n, for all positive n. *)
  