src/HOL/MiniML/W.thy
changeset 5184 9b8547a9496a
parent 4502 337c073de95e
child 14422 b8da5f258b04
equal deleted inserted replaced
5183:89f162de39cf 5184:9b8547a9496a
    15 (* type inference algorithm W *)
    15 (* type inference algorithm W *)
    16 
    16 
    17 consts
    17 consts
    18         W :: [expr, ctxt, nat] => result_W
    18         W :: [expr, ctxt, nat] => result_W
    19 
    19 
    20 primrec W expr
    20 primrec
    21   "W (Var i) A n =  
    21   "W (Var i) A n =  
    22      (if i < length A then Some( id_subst,   
    22      (if i < length A then Some( id_subst,   
    23 	                         bound_typ_inst (%b. TVar(b+n)) (A!i),   
    23 	                         bound_typ_inst (%b. TVar(b+n)) (A!i),   
    24 	                         n + (min_new_bound_tv (A!i)) )  
    24 	                         n + (min_new_bound_tv (A!i)) )  
    25 	              else None)"
    25 	              else None)"