Searched refs:ifn (Results 1 - 5 of 5) sorted by relevance
/seL4-l4v-10.1.1/l4v/tools/c-parser/testfiles/ |
H A D | automatic_modifies.c | 38 void ifn(int *p, int i) function 45 ifn(array2 + 3);
|
/seL4-l4v-10.1.1/HOL4/src/pfl/ |
H A D | pflLib.sml | 23 (* IS_SOME (ifn d args) ==> (ifn d args = ifn (SUC d) args) *) 43 val (ifn,args) = strip_comb ifn_app value 63 mk_eq (ifn_app,list_mk_comb(ifn,mk_suc d::args')))) 69 mk_eq(ifn_app,list_mk_comb(ifn,d1::args')))) 83 mk_eq(ifn_app, list_mk_comb(ifn,rdepth_app::args')))) 91 mk_is_some(list_mk_comb(ifn,d1::args'))), 92 mk_eq(ifn_app,list_mk_comb(ifn,d1::args'))))
|
H A D | index.sml | 305 (* Input: ifn 0 v0 ... vn = NONE *) 442 fun mk_rule ifn pfn = mk_thm([],``^ifn ^(mk_var("n",num)) = ^pfn``) 467 let val (ifn,args) = strip_comb(lhs goal) value 469 val subgoal = mk_is_some(list_mk_comb(ifn,suc_zero::args'))
|
/seL4-l4v-10.1.1/HOL4/src/list/src/ |
H A D | ListConv1.sml | 242 val ifn = itfn cnv thms value 252 in EQF_INTRO(itlist ifn (combine(l1,exd))(NOT_EQ_SYM thm1)) 261 in EQF_INTRO(itlist ifn (combine(exd,l2)) thm1) 263 else let val thm = itlist ifn (combine(l1,l2)) (REFL (Nil ty))
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | TypeBasePure.sml | 1021 fun ifn c = let val (_,ty') = dom_rng (type_of c) function 1025 val updfns' = map ifn updfns
|
Completed in 47 milliseconds