Searched refs:arg (Results 151 - 175 of 349) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/polyml/basis/
H A DExnPrinter.sml45 fun stringException(s, arg: string) =
46 parameterException(s, PolyML.prettyRepresentation(arg, depth-1))
/seL4-l4v-master/isabelle/src/Tools/jEdit/src/
H A Disabelle.scala433 (name, arg) <- Token.read_antiq_arg(Keyword.Keywords.empty, body_text)
440 if (arg.isEmpty) ""
441 else if (Isabelle_Encoding.is_active(buffer)) Symbol.cartouche_decoded(arg.get)
442 else Symbol.cartouche(arg.get)
/seL4-l4v-master/l4v/isabelle/src/Tools/jEdit/src/
H A Disabelle.scala433 (name, arg) <- Token.read_antiq_arg(Keyword.Keywords.empty, body_text)
440 if (arg.isEmpty) ""
441 else if (Isabelle_Encoding.is_active(buffer)) Symbol.cartouche_decoded(arg.get)
442 else Symbol.cartouche(arg.get)
/seL4-l4v-master/HOL4/src/compute/src/
H A DcomputeLib.sml57 * Precondition: f(arg) is a closure corresponding to b.
58 * Given (arg,(|- M = (a b), Stk)),
59 * returns (|- a = a, (<fun>,(|- b = b, f(arg)))::Stk)
62 fun push_in_stk f (arg,(th,stk)) =
64 (tha, Cbv_rator{Rand=(mka,(thb,f arg)), Ctx=stk})
67 fun push_skip_stk f (arg,(th,stk)) =
69 (tha, Cbv_rand{Rator=(Lib.C mka,true,(thb,f arg)), Ctx=stk})
98 - If the RHS is an abstraction and there is one arg on the stack, this means
/seL4-l4v-master/HOL4/examples/hardware/hol88/computer/
H A Dproof2.ml146 i n assumptions (buf,m,mar,pc,acc,ir,arg,mpc,ready) =
148 then (buf,m,mar,pc,acc,ir,arg,mpc,ready)
152 ([buf;m;mar;pc;acc;ir;arg;mpc] @ assumptions)
172 let (buf,m,mar,pc,acc,ir,arg,mpc,readylist) =
/seL4-l4v-master/HOL4/src/TeX/
H A Dholindex.lex2 type arg = int;
/seL4-l4v-master/HOL4/src/compute/examples/
H A DArith.sml39 * strongly (arg of a free var), but we will have to reduce the
/seL4-l4v-master/HOL4/src/portableML/
H A DArbrat.sml53 then raise Fail "inv: arg = 0"
/seL4-l4v-master/HOL4/tools/Holmake/
H A Dinternal_functions.sml247 fun which arg =
253 val fname = OS.Path.concat(p, arg)
270 fun shell arg =
286 val proc = execute ("/bin/sh", ["-c", arg])
H A DHolmake_tools.sml657 fun runholdep {ofs, extras, includes, arg, destination} = let
660 val _ = chatty ("Analysing "^fromFile arg)
676 val _ = diagK ("Running Holdep on "^fromFile arg^" with includes = [" ^
681 includes = includes, fname = fromFile arg}
774 val arg = holdep_arg f (* arg is file to analyse for dependencies *) value
777 if isSome arg then let
778 val arg = valOf arg value
779 val argname = fromFile arg
[all...]
/seL4-l4v-master/isabelle/src/Pure/Admin/
H A Dcomponents.scala290 "o:" -> (arg => options = options + arg),
H A Dbuild_fonts.scala351 "d:" -> (arg => source_dirs = source_dirs ::: List(Path.explode(arg))))
/seL4-l4v-master/isabelle/src/Pure/Tools/
H A Dsimplifier_trace.scala172 consume = (arg: Any) =>
174 arg match {
/seL4-l4v-master/HOL4/examples/temporal_deep/src/tools/
H A DcongToolsLib.sml39 val reflThm = refl {Rinst=preorderTerm,arg=var}
/seL4-l4v-master/l4v/isabelle/src/Pure/Admin/
H A Dcomponents.scala290 "o:" -> (arg => options = options + arg),
H A Dbuild_fonts.scala351 "d:" -> (arg => source_dirs = source_dirs ::: List(Path.explode(arg))))
/seL4-l4v-master/l4v/isabelle/src/Pure/Tools/
H A Dsimplifier_trace.scala172 consume = (arg: Any) =>
174 arg match {
/seL4-l4v-master/HOL4/tools/Holmake/mosml/
H A DBuildCommand.sml57 fun build_command g (ii as {preincludes,includes}) c arg = let
65 val file = fromFile arg
66 val intp = case arg of SML (Script _) => true | _ => false
/seL4-l4v-master/HOL4/src/parse/
H A Dtestutils.sml251 fun shouldfail {printarg,testfn,printresult,checkexn} arg =
253 val _ = tprint (printarg arg)
257 require_msg check printresult testfn arg
H A DParse_support.sml435 fun itthis (bvs, arg) {body_bvars,args,E} = let
437 val (arg',E') =
438 case rst of [] => arg E | L => bind_term l L arg E
440 {body_bvars = b::body_bvars, args=arg'::args, E=E'}
445 fun rev_itthis arg (core, E) =
449 (Comb{Rator= Comb{Rator=let_t, Rand=core,Locn=l},Rand=arg,Locn=l},
/seL4-l4v-master/HOL4/polyml/libpolyml/
H A Dbasicio.cpp163 POLYEXTERNALSYMBOL POLYUNSIGNED PolyChDir(FirstArgument threadId, PolyWord arg);
164 POLYEXTERNALSYMBOL POLYUNSIGNED PolyBasicIOGeneral(FirstArgument threadId, PolyWord code, PolyWord strm, PolyWord arg);
615 POLYUNSIGNED PolyChDir(FirstArgument threadId, PolyWord arg) argument
621 Handle pushedArg = taskData->saveVec.push(arg);
1066 POLYUNSIGNED PolyBasicIOGeneral(FirstArgument threadId, PolyWord code, PolyWord strm, PolyWord arg) argument
1074 Handle pushedArg = taskData->saveVec.push(arg);
/seL4-l4v-master/HOL4/src/AI/sml_inspection/
H A DsmlParallel.sml234 fun widarg_file pd wid = wid_dir pd wid ^ "/arg"
371 val arg = (#read_arg es) (widarg_file pd wid) value
372 val r = (#function es) param arg
427 write_arg = let fun f file arg = writel file [its arg] in f end,
/seL4-l4v-master/HOL4/examples/dev/sw2/
H A Ddefunctionalize.sml178 List.map (fn arg =>
180 Tyop = M.find(!ClosName, type_of arg)
181 handle e => #1 (Type.dest_type (type_of arg))})
286 val arg = mk_pair(clos_arg, f_arg) value
287 val lt = mk_comb(df_var, arg)
334 val (arg, body) = dest_pabs M value
335 val _ = convert_fun (mk_eq(mk_comb(v, arg), body))
/seL4-l4v-master/HOL4/tools/mlyacc/mlyacclib/
H A DMLY_parser2.sml222 fn (table,showTerminal,saction,fixError,arg) =>
244 (case saction(i,leftPos,stack,arg)
271 fn (table,showTerminal,saction,arg) =>
292 (case saction(i,leftPos,stack,arg)
535 val parse = fn {arg,table,lexer,saction,void,lookahead,
544 val distanceParse = distanceParse(table,showTerminal,saction,arg)
546 val ssParse = ssParse(table,showTerminal,saction,fixError,arg)
/seL4-l4v-master/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/
H A Dparser2.sml194 fn (table,showTerminal,saction,fixError,arg) =>
216 (case saction(i,leftPos,stack,arg)
243 fn (table,showTerminal,saction,arg) =>
264 (case saction(i,leftPos,stack,arg)
517 val parse = fn {arg,table,lexer,saction,void,lookahead,
526 val distanceParse = distanceParse(table,showTerminal,saction,arg)
528 val ssParse = ssParse(table,showTerminal,saction,fixError,arg)

Completed in 605 milliseconds

1234567891011>>