/seL4-l4v-master/HOL4/examples/hardware/hol88/computer/ |
H A D | proof5.ml | 13 % (mpc,mar,ir,arg,buf) % 114 (mpc,mar,ir,arg,buf)
|
H A D | proof1.ml | 158 % (mpc,mar,ir,arg,buf) % 179 % (mpc,mar,ir,arg,buf) % 545 % (mpc,mar,ir,arg,buf) %
|
/seL4-l4v-master/HOL4/src/IndDef/ |
H A D | CoIndDefLib.sml | 30 fun mk_def arg ant = 32 list_mk_abs(arg,list_mk_exists(rels',
|
/seL4-l4v-master/HOL4/src/datatype/mutrec/ |
H A D | ConsThms.sml | 270 has one arg, or CON_arg1 ... CON_argn if CON has n args), 371 fun define_single_ftn con arg = 372 let val appl_term = mk_comb {Rator = con, Rand = arg} 374 val arg_type = type_of arg 378 val def_clause = mk_eq {lhs = ftn_appl_term, rhs = arg} 397 fun helper count (arg::more_args) = 398 let val arg_type = type_of arg 404 val def_clause = mk_eq {lhs = ftn_appl_term, rhs = arg}
|
H A D | MutRecDef.sml | 272 is for. We build up the being_defined & existing constructor arg lists 413 arg = mk_select{Bvar = mk_var{Name = "x", Ty = ty}, 417 arg = mk_select (joint_select_x ty_name)} 429 {args = (#arg next) :: args, 555 foldr (fn (arg, range_ty) => mk_fun{Domain = type_of arg, 600 fun coerce_arg (arg, existing ty) = arg 601 | coerce_arg (arg, being_defined tyname) = 602 mk_comb {Rator = get_rep tyname, Rand = arg} [all...] |
/seL4-l4v-master/HOL4/src/parse/ |
H A D | Pretype.sml | 42 fun update arg E = 44 val E' = Env.update arg E
|
H A D | type_pp.sml | 216 pr_list (fn arg => pr_ty arg grav (depth - 1))
|
H A D | AncestryData.sml | 215 fun fullmake (arg as {adinfo:('delta,'value)adata_info,...}) = 218 val {adinfo, sexps, globinfo, uptodate_delta} = arg
|
/seL4-l4v-master/HOL4/src/pfl/examples/ |
H A D | zero.sml | 135 Q.PAT_ASSUM `IS_SOME arg` (MP_TAC o ONCE_REWRITE_RULE [izero_def]) THEN 143 Q.PAT_ASSUM `IS_SOME arg` (MP_TAC o ONCE_REWRITE_RULE [izero_def]) THEN
|
/seL4-l4v-master/HOL4/src/portableML/poly/ |
H A D | Intmap.sml | 151 fun peek arg = (SOME(retrieve arg)) handle NotFound => NONE
|
/seL4-l4v-master/HOL4/src/quantHeuristics/ |
H A D | quantHeuristicsLibAbbrev.sml | 145 EVERY_CONV (map (fn arg => TRY_CONV (try_select arg)) select_terms) t
|
/seL4-l4v-master/HOL4/tools/ |
H A D | configure-mosml.sml | 98 fun which arg = 104 val fname = OS.Path.concat(p, arg)
|
/seL4-l4v-master/HOL4/tools-poly/poly/ |
H A D | Binarymap.sml | 162 fun peek arg = (SOME(find arg)) handle NotFound => NONE
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ |
H A D | STRUCTVALSIG.sml | 72 arg: types, 132 arg: structVals,
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Atom.sml | 219 fun addArg ((n,arg),acc) = 223 List.foldl addTm acc (Term.nonVarTypedSubterms arg)
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Atom.sml | 219 fun addArg ((n,arg),acc) = 223 List.foldl addTm acc (Term.nonVarTypedSubterms arg)
|
/seL4-l4v-master/HOL4/tools-poly/ |
H A D | smart-configure.sml | 134 fun which arg = 140 val fname = OS.Path.concat(p, arg)
|
/seL4-l4v-master/HOL4/src/tactictoe/src/ |
H A D | tttEval.sml | 184 val argdir = gendir ^ "/arg"; 186 val (vnno,pnno,anno) = triple_of_list (map prefix ["val","pol","arg"]);
|
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | x86_dep.cpp | 203 virtual void InitStackFrame(TaskData *parentTask, Handle proc, Handle arg); 553 void X86TaskData::InitStackFrame(TaskData *parentTaskData, Handle proc, Handle arg) argument 578 assemblyInterface.p_rax = (arg == 0) ? TAGGED(0) : DEREFWORD(arg); // Argument
|
/seL4-l4v-master/HOL4/examples/ARM_security_properties/ |
H A D | ARM_proverLib.sml | 623 val (opr, arg) = 625 COMB (opr, arg) => (opr, arg) 630 [(SPECL [src_inv,arg, 632 (INST_TYPE [alpha |-> (type_of arg)]
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
H A D | TYPECHECK_PARSETREE.sml | 256 fun apply (f, arg, lex, location, moreInfo, typeEnv) = 258 FunctionType {arg=farg, result} => 260 unify (farg, arg, lex, location, moreInfo, typeEnv); 264 let (* Make arg->'a, and unify with the function. *) 266 val fType = mkFunctionType (arg, resType) 344 | nonExpansive (Applic{f, arg, ...}) = 345 isNonRefConstructor f andalso nonExpansive arg 567 | Applic {f = con, arg, location, expType, ...} => 609 val patType = processPattern(arg, enterResult, level, notConst, mkVar, isRec); 757 | Applic {f, arg, locatio [all...] |
H A D | PRINT_PARSETREE.sml | 161 | Applic { f, arg = TupleTree{fields=[left, right], ...}, isInfix = true, ...} => 173 | Applic {f, arg, ...} => (* Function application. *) 178 displayParsetree (arg, depth - 1)
|
/seL4-l4v-master/HOL4/src/1/ |
H A D | Pmatch.sml | 277 | mk_switch ((lit,arg)::litargs) = 278 if is_var lit then mk_comb(arg, v') 279 else mk_bool_case(arg, mk_switch litargs, mk_eq(v', lit)) 634 val (cases,arg) = 637 in case match_info tybase (type_names (type_of arg)) 643 val constrs_type = map (pair (type_of arg)) constrs 644 in (c, arg, map build_case_clause (zip constrs_type cases))
|
/seL4-l4v-master/HOL4/examples/HolCheck/ |
H A D | bddTools.sml | 108 (List.map (fn arg => 109 let val var = List.hd arg 110 val vl = List.last arg
|
/seL4-l4v-master/HOL4/examples/dev/sw/ |
H A D | funCall.sml | 82 | (arg, (t,i)) => (t, i+1) 331 (* | arg 3 | *) 332 (* | arg 2 | *) 333 (* sp | arg 1 | *)
|