/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | declFuncs.sml | 17 type func = {name : string, ftype : hol_type, ir : IRSyntax.exp * annotatedIR.anntIR * IRSyntax.exp, type
|
H A D | ANF.sml | 260 val (func,args) = value 335 val (func,args) = value 410 val (func,args) = dest_comb l value [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | declFuncs.sml | 17 type func = {name : string, ftype : hol_type, ir : IRSyntax.exp * annotatedIR.anntIR * IRSyntax.exp, type
|
H A D | ANF.sml | 260 val (func,args) = value 335 val (func,args) = value 410 val (func,args) = dest_comb l value [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
H A D | declFuncs.sml | 17 type func = {name : string, ftype : hol_type, ir : IRSyntax.exp * annotatedIR.anntIR * IRSyntax.exp, type
|
H A D | ACF.sml | 204 val (func,args) = value 253 val (func,args) = dest_comb lt value 318 val (func,args) = dest_comb l value [all...] |
H A D | ANF.sml | 260 val (func,args) = value 335 val (func,args) = value 410 val (func,args) = dest_comb l value [all...] |
/seL4-l4v-10.1.1/seL4/src/arch/arm/smp/ |
H A D | ipi.c | 22 static inline void init_ipi_args(IpiModeRemoteCall_t func, argument
|
/seL4-l4v-10.1.1/seL4/src/smp/ |
H A D | ipi.c | 87 void doRemoteMaskOp(IpiRemoteCall_t func, word_t data1, word_t data2, word_t data3, word_t mask) argument
|
/seL4-l4v-10.1.1/seL4/src/arch/x86/smp/ |
H A D | ipi.c | 22 static inline void init_ipi_args(IpiModeRemoteCall_t func, argument
|
/seL4-l4v-10.1.1/HOL4/src/coretypes/ |
H A D | pairTools.sml | 259 let val (func,arg) = dest_let w value
|
H A D | PairedLambda.sml | 254 val (func, arg) = boolSyntax.dest_let tm value
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | metisTools.sml | 86 val {func,pred} = fix N value
|
H A D | mlibModel.sml | 65 val {func = func1, pred = pred1} = fix1 N value 66 val {func = func2, pred = pred2} = fix2 N value 67 fun func x = case func1 x of NONE => func2 x | sn => sn function 77 val {func,pred} = fix N value 89 fun func ("id",[n]) = SOME n function 116 fun func ("0",[]) = SOME zero function 147 fun func ("0",[]) = SOME zero function 180 fun func ("empty",[]) = SOME (from_set empty) function 309 val {func = fixf, pred = fixp} = r n value [all...] |
H A D | mlibTerm.sml | 522 fun func fs [] = fs function [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/ |
H A D | inlineCompile.sml | 90 val (func,args) = dest_comb lt value 214 let val (func,_) = value
|
/seL4-l4v-10.1.1/HOL4/src/new-datatype/ |
H A D | Witness.sml | 150 val func = fn (i, (wit, res)) => ( value
|
H A D | NDatatype.sml | 81 val func = INST_TYPE[alpha|->ty, beta|->self] value 204 val func = fn (x,l) => RIGHT_LIST_BETA (REFL (list_mk_comb(list_mk_abs(l, x), l))) value 241 val func = fn (w, (x, (y, z))) => gen_rich_tyvar w x y z value 388 val func = fn x => (PURE_REWRITE_RULE [mythm] x value 406 val func = fn (s,ax) => define_new_type_bijections value [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
H A D | sighandler.cpp | 413 bool setSignalHandler(int sig, signal_handler_type func) argument
|
H A D | interpret.cpp | 136 virtual Handle EnterCallbackFunction(Handle func, Handle args) { ASSERT(0); return 0; } argument
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/ |
H A D | closures.c | 389 int (*func)(const char *); member in struct:__anon34
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | CODETREE_STATIC_LINK_AND_CASES.sml | 118 val func = locaddr(LoadRecursive, (* closure = *) false) value 139 val func = locaddr(ext, (* closure = *) false) value 173 val func = copyProcClosure (copiedLambda, newClosure, makeRecClosure) value 182 val func = insert function value
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | Preterm.sml | 832 val func = snd (dest_abs functional) value
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
H A D | acl2encodeLib.sml | 787 val func = foldr pairLib.mk_pair_map (last decoders) (butlast decoders) value
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Term.sml | 57 fun func fs [] = fs function 66 fun func fs [] = fs function [all...] |