anchor.diff:  type inductiveConstructor = {
     cname: lident;
     ctype : typ;
  -  cargs : binders (*will this list always be empty? it has always been empty: tested nat, list, vec*)
  +  cargs : binders (*will this list always be empty? it has always been empty so far*)
   }
   type inductiveTypeFam = {
     tyName: lident;
  
positive.code:         let bts = extractBindersTypes c bs in
          (let codomainML = (extractComp  c codomain) in 
          if  (codomainML = erasedContent) 
          then erasedContent 
          else  (curry bts codomainML))
  
    | Typ_refine (bv (*var and unrefined type*) , _ (*refinement condition*)) -> extractTyp c bv.sort
  
    (*can this be a partial type application? , i.e can the result of this application be something like Type -> Type, or nat -> Type? : Yes *)
    | Typ_app (ty, arrgs) ->
      (match ty.n with
          | Typ_btvar btv -> (if (contains c btv) then MLTY_Var (prependTick (convIdent btv.v.ppname)) else unknownType)
  
negative.code: let convRange (r:Range.range) : int = 0 (*FIX!!*)
  let convIdent (id:ident) : mlident = (id.idText ,(convRange id.idRange))
      
  type argTransform = arg -> option<arg> (*none indicates that this argument should be deleted*)
  type nthArgTransform = int -> argTransform (* f n is the argtransform for the nth argument (of a type constant)*)
  let idArgTransform :argTransform = fun a -> Some a
  type nthArgTransforms = lident (*name of a constant*) -> nthArgTransform
   
  
  type context = {
    e : env;
    at:nthArgTransforms
  }
  
  (* vars in tyVars will have type Type, irrespective of that types they had in F*. This is to match the limitations of  OCaml*)
  let extendContext (c:context) (tyVars : list<binder>) : context = 
  {
    e= List.fold push_local_binding c.e (List.map binding_of_binder tyVars);
    at= c.at
  }
  
  let contains (c:context) (b:btvar) : bool = 
    try (let _ = (lookup_btvar c.e b) in true) (*does not work for vars mentioned in bodies of inductives. those mentions have wierd chars appended in realnames. their range matches, though*)
    with
     | _ -> false
  
  