Searched refs:arg (Results 101 - 125 of 349) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/src/1/
H A DRsyntax.sml23 fun mk_let{func,arg} = boolSyntax.mk_let(func,arg)
50 fun dest_let M = let val (f,a) = boolSyntax.dest_let M in {func=f,arg=a} end;
H A DRsyntax.sig22 val mk_let : {arg:term, func:term} -> term
39 val dest_let : term -> {arg:term, func:term}
/seL4-l4v-master/HOL4/src/bag/
H A DbagSyntax.sml98 val (f, arg) = dest_comb tm
102 arg
110 val (f, arg) = dest_comb tm
114 arg
/seL4-l4v-master/HOL4/tools/mlyacc/src/
H A Dparse.sml28 sharing type Parser.arg = Header.inputSource =
/seL4-l4v-master/HOL4/src/tactictoe/src/
H A DtttTrain.sml152 fun nntm_of_arg arg = case arg of
156 fun nntm_of_statearg ((g,stac),arg) =
158 mk_binop gstacarg_cat (nntm_of_gstac (g,stac), nntm_of_arg arg))
/seL4-l4v-master/HOL4/src/coretypes/
H A DPairedLambda.sml91 let val (abst,arg) = dest_comb tm
95 val eqv = if can dest_pair arg then REFL arg else ISPEC arg pair
254 val (func, arg) = boolSyntax.dest_let tm
257 val thm = RIGHT_BETA (AP_THM (RIGHT_BETA (AP_THM defn func)) arg)
260 then REDUCE func arg (RIGHT_BETA thm)
266 (AP_TERM (rator (rator tm)) (conv bconv func)) arg)
H A DpairLib.sml20 (* given (��(x,y,...) ...) arg (UOK)
22 arg = (x,y,...)
31 (* ?x y z ... . arg = (x,y,z,...) *)
/seL4-l4v-master/HOL4/help/src-sml/
H A DLexer.lex2 type arg = int;
182 %arg (commentDepth);
/seL4-l4v-master/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/
H A Dparser1.sml44 val parse = fn {arg : 'a,
83 saction(i,leftPos,stack,arg)
/seL4-l4v-master/l4v/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/
H A Dparser1.sml44 val parse = fn {arg : 'a,
83 saction(i,leftPos,stack,arg)
/seL4-l4v-master/HOL4/examples/dev/sw/
H A DAssem.sml265 List.map (fn arg => print (one_exp arg ^ " ")) (pair2list args);
267 List.map (fn arg => print (one_exp arg ^ " ")) (Binaryset.listItems rs);
269 List.map (fn arg => print (one_exp arg ^ " ")) (pair2list outs);
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/
H A DAssem.sml265 List.map (fn arg => print (one_exp arg ^ " ")) (pair2list args);
267 List.map (fn arg => print (one_exp arg ^ " ")) (Binaryset.listItems rs);
269 List.map (fn arg => print (one_exp arg ^ " ")) (pair2list outs);
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/
H A DAssem.sml265 List.map (fn arg => print (one_exp arg ^ " ")) (pair2list args);
267 List.map (fn arg => print (one_exp arg ^ " ")) (Binaryset.listItems rs);
269 List.map (fn arg => print (one_exp arg ^ " ")) (pair2list outs);
/seL4-l4v-master/HOL4/src/simp/src/
H A DcongLib.sml53 fun gen_refl(x as {Rinst,arg}) = mk_preorder_refl preorders Rinst x
64 val reflThm = refl {Rinst=preorderTerm,arg=var}
77 val reflThm = refl {Rinst=preorderTerm,arg=var}
83 (CONGPROC (fn {Rinst,arg} => REFL arg)) thm
288 fun conv thms tm = qconv thms tm handle _ => refl {Rinst=relation,arg=tm}
/seL4-l4v-master/HOL4/examples/separationLogic/src/
H A DseparationLogicSyntax.sml177 val arg = strip_comb_1 COND_PROP___STRONG_EXISTS_term tt; value
178 val (v, body) = pairSyntax.dest_pabs arg
189 val arg = strip_comb_1 COND_PROP___EXISTS_term tt; value
190 val (v,b) = dest_abs arg
243 val arg = strip_comb_1 asl_exists_term tt; value
244 val (v,b) = dest_abs arg
/seL4-l4v-master/isabelle/src/Pure/Admin/
H A Dbuild_status.scala602 "D:" -> (arg => target_dir = Path.explode(arg)),
604 "S:" -> (arg => only_sessions = space_explode(',', arg).toSet),
605 "l:" -> (arg => options = options + ("build_log_history=" + arg)),
606 "o:" -> (arg => options = options + arg),
607 "s:" -> (arg =>
608 space_explode('x', arg)
[all...]
/seL4-l4v-master/l4v/isabelle/src/Pure/Admin/
H A Dbuild_status.scala602 "D:" -> (arg => target_dir = Path.explode(arg)),
604 "S:" -> (arg => only_sessions = space_explode(',', arg).toSet),
605 "l:" -> (arg => options = options + ("build_log_history=" + arg)),
606 "o:" -> (arg => options = options + arg),
607 "s:" -> (arg =>
608 space_explode('x', arg)
[all...]
/seL4-l4v-master/HOL4/src/datatype/mutrec/
H A DRecftn.sml35 constructed with that constructor. If there is a variable "arg" with
230 let fun apply_all ftn (arg::args) =
231 apply_all (mk_comb {Rator = ftn, Rand = arg}) args
254 variable "arg" in order to allow the uxser to do something
259 let val arg_var = mk_var {Name = "arg", Ty = ftn_dom}
376 type atpat (since it's the second arg to constructor CONpat), and
404 fun get_rec_vars (all_vars, arg::more_args, rev_rec_vars) =
405 let val ftn_info = lookup_ftn (type_of arg, ftn_type_data)
409 (* can't recurse on this arg, so add no more vars *)
431 fun sort_cons_args (arg
[all...]
/seL4-l4v-master/HOL4/examples/hardware/hol88/tamarack2/
H A Dtamarack.ml116 (mem,mar,pc,acc,ir,arg,buf)) =
127 REG ((warg,gnd,bus,bus,arg),P) /\
128 ALU (n+3) (alu0,alu1,arg,bus,alu) /\
227 "Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) =
237 (mem,mar,pc,acc,ir,arg,buf))");;
/seL4-l4v-master/HOL4/examples/hardware/port/tamarack2/
H A DtamarackScript.sml112 (mem,mar,pc,acc,ir,arg,buf)) =
123 REG ((warg,gnd,bus,bus,arg),P) /\
124 ALU (n+3) (alu0,alu1,arg,bus,alu) /\
223 ``Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) =
233 (mem,mar,pc,acc,ir,arg,buf))``);
/seL4-l4v-master/HOL4/examples/elliptic/c_output/
H A Dc_outputLib.sml241 ((not (all (fn arg => (type_of arg = word_type)) args))))
273 fun translate_args arg =
274 if (numLib.is_numeral arg) then
275 ([], [term_to_string arg])
279 get_word_fun_arity (type_of arg);
282 ("Invalid argument '" ^ (term_to_string arg) ^"' in term '"^(term_to_string exp)^"'!");
284 translate_exp arg res_n
486 val args_string_list = map (fn arg =>
487 word_type_string^ " "^(#1 (dest_var arg))) args_lis
[all...]
/seL4-l4v-master/HOL4/examples/HolCheck/examples/
H A Damba_apb.sml42 fun apb_PSEL_proj i = if i<4 then apb_AP ("psel_"^(int_to_string i)) else failwith ("apb_PSEL_proj arg out of range")
52 fun apb_SADDR x = if x<2 then (apb_AP ("saddr_"^(int_to_string x))) else failwith ("apb_SADDR arg out of range")
53 fun apb_SDATA x = if x<2 then (apb_AP ("sdata_"^(int_to_string x))) else failwith ("apb_SDATA arg out of range")
/seL4-l4v-master/HOL4/polyml/libpolyml/
H A Dtiming.cpp124 POLYEXTERNALSYMBOL POLYUNSIGNED PolyTimingLocalOffset(FirstArgument threadId, PolyWord arg);
125 POLYEXTERNALSYMBOL POLYUNSIGNED PolyTimingSummerApplies(FirstArgument threadId, PolyWord arg);
126 POLYEXTERNALSYMBOL POLYUNSIGNED PolyTimingConvertDateStuct(FirstArgument threadId, PolyWord arg);
283 POLYUNSIGNED PolyTimingLocalOffset(FirstArgument threadId, PolyWord arg) argument
289 Handle pushedArg = taskData->saveVec.push(arg);
354 POLYUNSIGNED PolyTimingSummerApplies(FirstArgument threadId, PolyWord arg) argument
360 Handle pushedArg = taskData->saveVec.push(arg);
399 POLYUNSIGNED PolyTimingConvertDateStuct(FirstArgument threadId, PolyWord arg) argument
405 Handle pushedArg = taskData->saveVec.push(arg);
/seL4-l4v-master/HOL4/tools/mlyacc/mlyacclib/
H A DMLY_parser1.sml66 val parse = fn {arg : 'a,
105 saction(i,leftPos,stack,arg)
/seL4-l4v-master/HOL4/polyml/
H A Dinstall-sh180 for arg
183 # $@ is not empty: it contains at least $arg.
187 shift # arg
188 dst_arg=$arg

Completed in 170 milliseconds

1234567891011>>