/seL4-l4v-master/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 | 256 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 D | declFuncs.sml | 17 type func = {name : string, ftype : hol_type, ir : IRSyntax.exp * annotatedIR.anntIR * IRSyntax.exp, type
|
H A D | ANF.sml | 256 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 D | declFuncs.sml | 17 type func = {name : string, ftype : hol_type, ir : IRSyntax.exp * annotatedIR.anntIR * IRSyntax.exp, type
|
H A D | ACF.sml | 202 val (func,args) = value 251 val (func,args) = dest_comb lt value 316 val (func,args) = dest_comb l value [all...] |
H A D | ANF.sml | 256 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 D | ipi.c | 16 static inline void init_ipi_args(IpiRemoteCall_t func, argument
|
/seL4-l4v-master/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-master/seL4/src/arch/x86/smp/ |
H A D | ipi.c | 16 static inline void init_ipi_args(IpiRemoteCall_t func, argument
|
/seL4-l4v-master/seL4/src/arch/riscv/smp/ |
H A D | ipi.c | 18 static inline void init_ipi_args(IpiRemoteCall_t func, argument
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | metisTools.sml | 86 val {func,pred} = fix N value
|
H A D | mlibModel.sml | 66 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 D | mlibTerm.sml | 522 fun func fs [] = fs function [all...] |
/seL4-l4v-master/HOL4/src/coretypes/ |
H A D | pairTools.sml | 271 let val (func,arg) = dest_let w value
|
H A D | PairedLambda.sml | 254 val (func, arg) = boolSyntax.dest_let tm value
|
/seL4-l4v-master/HOL4/examples/dev/ |
H A D | inlineCompile.sml | 90 val (func,args) = dest_comb lt value 214 let val (func,_) = value
|
/seL4-l4v-master/HOL4/src/new-datatype/ |
H A D | Witness.sml | 150 val func = fn (i, (wit, res)) => ( value
|
H A D | NDatatype.sml | 80 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 D | sighandler.cpp | 402 bool setSignalHandler(int sig, signal_handler_type func) argument
|
/seL4-l4v-master/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-master/HOL4/examples/acl2/ml/ |
H A D | acl2encodeLib.sml | 787 val func = foldr pairLib.mk_pair_map (last decoders) (butlast decoders) value
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Term.sml | 57 fun func fs [] = fs function 66 fun func fs [] = fs function [all...] |
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Term.sml | 57 fun func fs [] = fs function 66 fun func fs [] = fs function [all...] |
/seL4-l4v-master/HOL4/src/parse/ |
H A D | Preterm.sml | 836 val func = snd (dest_abs functional) value
|