/seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/ |
H A D | Metafile.sml | 73 (* TODO: Many of these should check for NULL as a result indicating an error. *) 239 (* Initial call with a NULL buffer to get size and check the handle. *)
|
H A D | Transform.sml | 191 (* Should check the result is non-zero. *) 200 check GetLastError because the result could legitimately be zero. *)
|
/seL4-l4v-10.1.1/HOL4/src/num/ |
H A D | numLib.sml | 46 val check = assert (fn tm => type_of tm = N) value 51 val n = check Bvar
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | problem.py | 229 # check if the head point is a split (the inner loop 230 # check does exactly that) 771 check = [(head, p.loop_body (head)) for head in heads] 772 while check: 773 (head, body) = check.pop () 776 check.extend ([(head, [head] + list (body))
|
H A D | trace_refute.py | 17 import check namespace 119 p = check.build_problem (pair, avoid_abort = True) 127 """mirrors build_problem from check for multiple functions""" 154 free_hyps += check.inst_eqs (p, (), inp_eqs, tags)
|
/seL4-l4v-10.1.1/HOL4/examples/miller/ho_prover/ |
H A D | unifyTools.sml | 54 else if occurs ty1 ty2 then raise ERR "type_unify" "occurs check" 202 val _ = assert (not (occurs v' tm')) (ERR "unify" "occurs check")
|
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/ |
H A D | MMUScript.sml | 32 - check MMU_support for needed section descriptors only 37 - correct/check case analysis of permitted_byte
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | metis.sml | 132 fun check () = function 139 check
|
H A D | Model.sml | 1081 (* Note: if it's cheaper, a systematic check will be performed instead. *) 1084 fun check interpret {maxChecks} M fv x = function 1107 check interpretAtom maxChecks M (Atom.freeVars atm) atm; 1110 check interpretFormula maxChecks M (Formula.freeVars fm) fm; 1113 check interpretLiteral maxChecks M (Literal.freeVars lit) lit; 1116 check interpretClause maxChecks M (LiteralSet.freeVars cl) cl;
|
H A D | selftest.sml | 446 (* Bug check: in this one a literal goes missing, due to the Resolve in Subst *) 451 (* Bug check: term paths were not being reversed before use *) 456 (* Bug check: Equality used to complain if the literal didn't exist *) 1094 fun check ({name,goal,...}, acc) = function 1121 val _ = List.foldl check [] p
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | metis.sml | 132 fun check () = function 139 check
|
H A D | Model.sml | 1081 (* Note: if it's cheaper, a systematic check will be performed instead. *) 1084 fun check interpret {maxChecks} M fv x = function 1107 check interpretAtom maxChecks M (Atom.freeVars atm) atm; 1110 check interpretFormula maxChecks M (Formula.freeVars fm) fm; 1113 check interpretLiteral maxChecks M (Literal.freeVars lit) lit; 1116 check interpretClause maxChecks M (LiteralSet.freeVars cl) cl;
|
H A D | selftest.sml | 446 (* Bug check: in this one a literal goes missing, due to the Resolve in Subst *) 451 (* Bug check: term paths were not being reversed before use *) 456 (* Bug check: Equality used to complain if the literal didn't exist *) 1094 fun check ({name,goal,...}, acc) = function 1121 val _ = List.foldl check [] p
|
/seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
H A D | Yices.sml | 8 a numeric constant, etc. We do not check these side conditions on 246 (* check table of types *) 335 (* Hopefully used as index into a bit vector, but we don't check -- Yices 613 (* FIXME: This check for matching types may be too liberal, as it 648 (* FIXME: This check for matching types may be too liberal, as it 762 defs @ yices_asl_g @ ["(check)\n"]
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | normalForms.sml | 1299 fun check best [] = best function 1300 | check best ((f, form) :: rest) = 1317 check best rest 1327 check best rest 1337 check best rest 1339 | break best _ Lit rest = check best rest; 1341 val min_cnf_search = check;
|
H A D | mlibUseful.sml | 518 fun check s = assert (String.isPrefix p s) (Error "dest_prefix") function 521 fn s => (check s; String.extract (s, size_p, NONE))
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | Tactical.sml | 257 * Fail with the given token. Useful in tactic programs to check that a 366 fun check ths gls = function 373 NONE => check ths0 gls0 376 check (prf (map masquerade glist)) gl 775 * we should do this check in the hypotheses of the goal as well.
|
H A D | boolSyntax.sml | 405 val check = value 417 val _ = check op2
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | type_grammar.sml | 261 val (check,privrm) = value 269 |> fupdate_str_print (TypeNet.fold (printmap check) TypeNet.empty) 271 (Binarymap.foldl (parsemap check)
|
/seL4-l4v-10.1.1/HOL4/src/real/ |
H A D | realSimps.sml | 568 fun check tm = function 574 RCACHE (dpvars, check,CTXT_ARITH) 575 (* the check function determines whether or not a term might be handled
|
H A D | RealArith.sml | 50 fun check f = if !traceval > 0 then f() else () function 66 fun trace s = check (trace_pure (s ^ "\n")) 67 fun trace_term t = check (trace_term_pure t >> trace_line) 69 check (trace_list_pure trace_term_pure l >> trace_line) 70 fun trace_thm t = check (trace_thm_pure t >> trace_line) 71 fun trace_thm_list l = check (trace_list_pure trace_thm_pure l >> trace_line)
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
H A D | encodeLib.sml | 45 fun check value t = function 53 check (itdeep (fn n => construct_bottom_value_n n p xvar t) 0 1476 val check = check_function (get_encode_function target) t value 1479 if can (match_term check) (rator term) then 1487 val check = check_function get_map_function t value 1490 if can (match_term check) (rator term) then 1497 val check = check_function get_all_function t value 1500 if can (match_term check) (rator term) then 1508 val check = check_function (get_decode_function target) t value 1542 if can (match_term check) (rato 1551 val check = check_function (get_detect_function target) t value [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | Int.sml | 70 (* If int is fixed precision we have to check that the value will fit. *) 339 (* If int is arbitrary precision we have to check that the value will fit. *) 348 (* When converting from arbitrary precision we have to check. *)
|
/seL4-l4v-10.1.1/isabelle/src/Pure/PIDE/ |
H A D | rendering.scala | 456 check: (Boolean, Long) => Boolean = (is_def: Boolean, i: Long) => is_def): Set[Long] = 463 case Markup.Entity.Def(i) if check(true, i) => Some(serials + i) 464 case Markup.Entity.Ref(i) if check(false, i) => Some(serials + i)
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/PIDE/ |
H A D | rendering.scala | 456 check: (Boolean, Long) => Boolean = (is_def: Boolean, i: Long) => is_def): Set[Long] = 463 case Markup.Entity.Def(i) if check(true, i) => Some(serials + i) 464 case Markup.Entity.Ref(i) if check(false, i) => Some(serials + i)
|