Searched defs:func (Results 1 - 25 of 32) sorted by relevance

12

/seL4-l4v-master/HOL4/examples/dev/sw/
H A DdeclFuncs.sml17 type func = {name : string, ftype : hol_type, ir : IRSyntax.exp * annotatedIR.anntIR * IRSyntax.exp, type
H A DANF.sml256 val (func,args) = value
331 val (func,args) = value
406 val (func,args) = dest_comb l value
[all...]
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/
H A DdeclFuncs.sml17 type func = {name : string, ftype : hol_type, ir : IRSyntax.exp * annotatedIR.anntIR * IRSyntax.exp, type
H A DANF.sml256 val (func,args) = value
331 val (func,args) = value
406 val (func,args) = dest_comb l value
[all...]
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/
H A DdeclFuncs.sml17 type func = {name : string, ftype : hol_type, ir : IRSyntax.exp * annotatedIR.anntIR * IRSyntax.exp, type
H A DACF.sml202 val (func,args) = value
251 val (func,args) = dest_comb lt value
316 val (func,args) = dest_comb l value
[all...]
H A DANF.sml256 val (func,args) = value
331 val (func,args) = value
406 val (func,args) = dest_comb l value
[all...]
/seL4-l4v-master/seL4/src/arch/arm/smp/
H A Dipi.c16 static inline void init_ipi_args(IpiRemoteCall_t func, argument
/seL4-l4v-master/seL4/src/smp/
H A Dipi.c87 void doRemoteMaskOp(IpiRemoteCall_t func, word_t data1, word_t data2, word_t data3, word_t mask) argument
/seL4-l4v-master/seL4/src/arch/x86/smp/
H A Dipi.c16 static inline void init_ipi_args(IpiRemoteCall_t func, argument
/seL4-l4v-master/seL4/src/arch/riscv/smp/
H A Dipi.c18 static inline void init_ipi_args(IpiRemoteCall_t func, argument
/seL4-l4v-master/HOL4/src/metis/
H A DmetisTools.sml86 val {func,pred} = fix N value
H A DmlibModel.sml66 val {func = func1, pred = pred1} = fix1 N value
67 val {func = func2, pred = pred2} = fix2 N value
68 fun func x = case func1 x of NONE => func2 x | sn => sn function
78 val {func,pred} = fix N value
90 fun func ("id",[n]) = SOME n function
117 fun func ("0",[]) = SOME zero function
148 fun func ("0",[]) = SOME zero function
181 fun func ("empty",[]) = SOME (from_set empty) function
310 val {func = fixf, pred = fixp} = r n value
[all...]
H A DmlibTerm.sml522 fun func fs [] = fs function
[all...]
/seL4-l4v-master/HOL4/src/coretypes/
H A DpairTools.sml271 let val (func,arg) = dest_let w value
H A DPairedLambda.sml254 val (func, arg) = boolSyntax.dest_let tm value
/seL4-l4v-master/HOL4/examples/dev/
H A DinlineCompile.sml90 val (func,args) = dest_comb lt value
214 let val (func,_) = value
/seL4-l4v-master/HOL4/src/new-datatype/
H A DWitness.sml150 val func = fn (i, (wit, res)) => ( value
H A DNDatatype.sml80 val func = INST_TYPE[alpha|->ty, beta|->self] value
203 val func = fn (x,l) => RIGHT_LIST_BETA (REFL (list_mk_comb(list_mk_abs(l, x), l))) value
240 val func = fn (w, (x, (y, z))) => gen_rich_tyvar w x y z value
387 val func = fn x => (PURE_REWRITE_RULE [mythm] x value
405 val func = fn (s,ax) => define_new_type_bijections value
[all...]
/seL4-l4v-master/HOL4/polyml/libpolyml/
H A Dsighandler.cpp402 bool setSignalHandler(int sig, signal_handler_type func) argument
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/
H A DCODETREE_STATIC_LINK_AND_CASES.sml118 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-master/HOL4/examples/acl2/ml/
H A Dacl2encodeLib.sml787 val func = foldr pairLib.mk_pair_map (last decoders) (butlast decoders) value
/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DTerm.sml57 fun func fs [] = fs function
66 fun func fs [] = fs function
[all...]
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DTerm.sml57 fun func fs [] = fs function
66 fun func fs [] = fs function
[all...]
/seL4-l4v-master/HOL4/src/parse/
H A DPreterm.sml836 val func = snd (dest_abs functional) value

Completed in 400 milliseconds

12