anchor.diff:  
       /// Creates an S-expression from an operator string, operand print function, and
       /// sequence of operands.
  -    let sexpr op pxs =
  +    let sexpr (op : string) (pxs : 'x -> Doc) : 'x seq -> Doc =
           Seq.map pxs
           >> scons (String op)
           >> hsep
           >> parened
   
       /// Pretty-prints an arithmetic expression.
  -    let rec printIntExpr pVar =
  +    let rec printIntExpr (pVar : 'var -> Doc) : IntExpr<'var> -> Doc =
           function
           | AVar c -> pVar c
           | AInt i -> i |> sprintf "%i" |> String
  
positive.code: 
  /// Returns true if the expression is definitely false.
  /// This is sound, but not complete.
  let isFalse expr =
      match (simp expr) with
      | BFalse -> true
      | _      -> false
  
  let isTrue expr =
      match (simp expr) with
      | BTrue -> true
      | _     -> false
  
  /// Converts a typed string to an expression.
  let mkVarExp marker (ts : CTyped<string>) =
      match ts with
      | Int s -> s |> marker |> AVar |> Int
      | Bool s -> s |> marker |> BVar |> Bool
  
  /// Converts a VarMap to a sequence of expressions.
  let varMapToExprs marker vm =
      vm |> Map.toSeq |> Seq.map (fun (name, ty) -> mkVarExp marker (withType ty name))
  
  (* The following are just curried versions of the usual constructors. *)
  
  /// Curried wrapper over BGt.
  let mkGt a b = BGt (a, b)
  /// Curried wrapper over BGe.
  let mkGe a b = BGe (a, b)
  /// Curried wrapper over BLt.
  let mkLt a b = BLt (a, b)
  /// Curried wrapper over BLe.
  let mkLe a b = BLe (a, b)
  
  /// Curried wrapper over BEq.
  let mkEq a b = BEq (a, b)
  
  /// Makes an arithmetic equality.
  let iEq a b = BEq (Int a, Int b)
  ///
  /// Makes an arithmetic addition
  let iAdd a b = AAdd [a ; b]
  
  /// Makes a Boolean equality.
  let bEq a b = BEq (Bool a, Bool b)
  
  /// Curried wrapper over ADiv.
  let mkDiv a b = ADiv (a, b)
  
  /// Slightly optimised version of ctx.MkAnd.
  /// Returns true for the empty array, and x for the singleton set {x}.
  let mkAnd xs = simp (BAnd xs)
  
  /// Slightly optimised version of ctx.MkOr.
  /// Returns false for the empty set, and x for the singleton set {x}.
  let mkOr xs = simp (BOr xs)
  
  /// Makes an And from a pair of two expressions.
  let mkAnd2 l r = mkAnd [l ; r]
  
  /// Makes an Or from a pair of two expressions.
  let mkOr2 l r = mkOr [l ; r]
  
  /// Symbolically inverts a Boolean expression.
  let mkNot x = simp (BNot x)
  
  /// Makes not-equals.
  let mkNeq l r = mkEq l r |> mkNot
  
  /// Makes an implication from a pair of two expressions.
  let mkImplies l r = BImplies (l, r) |> simp
  
  /// Makes an Add out of a pair of two expressions.
  let mkAdd2 l r = AAdd [ l; r ]
  /// Makes a Sub out of a pair of two expressions.
  let mkSub2 l r = ASub [ l; r ]
  /// Makes a Mul out of a pair of two expressions.
  let mkMul2 l r = AMul [ l; r ]
  
  
  (*
  
negative.code:         | ADiv (x, y) -> sexpr "/" (printIntExpr pVar) [x; y]
  
      /// Pretty-prints a Boolean expression.
      and printBoolExpr (pVar : 'var -> Doc) : BoolExpr<'var> -> Doc =
          function
          | BVar c -> pVar c
          | BTrue -> String "true"
  