anchor.diff:      subst=[];
       guard=Trivial;
       ctr=0;
  +    slack_vars=[];
  +    defer_ok=true;
   }
   let singleton prob         = {empty_worklist with attempting=[prob]}
   let extend_subst' uis wl   = {wl with subst=uis@wl.subst; ctr=wl.ctr + 1}
  
positive.code:    See the License for the specific language governing permissions and
     limitations under the License.
  *)
  #light "off"
  module Microsoft.FStar.Tc.Rel
  
  
negative.code: 
              | _ -> None) //not a pattern
  
  let destruct_flex_t t = match t.n with
      | Typ_uvar(uv, k) -> (t, uv, k, [])
      | Typ_app({n=Typ_uvar(uv, k)}, args) -> (t, uv, k, args)
      | _ -> failwith "Not a flex-uvar"
  (* ------------------------------------------------ *)
  (* </variable ops>                                  *)
  (* ------------------------------------------------ *)
  