Searched refs:ifn (Results 1 - 5 of 5) sorted by relevance

/seL4-l4v-10.1.1/l4v/tools/c-parser/testfiles/
H A Dautomatic_modifies.c38 void ifn(int *p, int i) function
45 ifn(array2 + 3);
/seL4-l4v-10.1.1/HOL4/src/pfl/
H A DpflLib.sml23 (* 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 Dindex.sml305 (* 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 DListConv1.sml242 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 DTypeBasePure.sml1021 fun ifn c = let val (_,ty') = dom_rng (type_of c) function
1025 val updfns' = map ifn updfns

Completed in 47 milliseconds