Searched refs:check (Results 51 - 75 of 382) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmlibSubst.sml102 fun check (a, b, (c, d)) = function
104 val (removed, dict') = M.foldl check (false, dict) dict
H A DmlibUnits.sml52 fun check t = (unify_literals |<>| (dest_unit t) lit, t) function
54 case first (total check) (N.unify uns lit) of NONE => NONE
H A DmlibModel.sig45 val check : model -> formula -> bool value
/seL4-l4v-10.1.1/HOL4/src/quantHeuristics/
H A DquantHeuristicsLibSimple.sig75 function to apply, a check when to apply and a theorem about how
76 to rewrite in case the check succeeds. For FST the entries would
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/model_check/
H A DmodelCheckLib.sig5 used to translate several model checking problems to a check for the
7 is used to check these properties. At the moment SMV and temporalLib by
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/testsuite/lib/
H A Dlibffi.exp332 proc check-flags { args } {
376 if [check-flags $args] {
/seL4-l4v-10.1.1/isabelle/src/Pure/General/
H A Dfile.scala155 def check(file: JFile) { if (pred(file)) result += file }
157 if (start.isFile) check(start)
163 if (include_dirs) check(path.toFile)
168 check(path.toFile)
/seL4-l4v-10.1.1/isabelle/src/Pure/Tools/
H A Dbuild_docker.scala91 echo = true).check
/seL4-l4v-10.1.1/isabelle/src/Tools/VSCode/src/
H A Dvscode_spell_checker.scala51 if (spell_checker.check(word))
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/
H A Djedit_spell_checker.scala60 if (spell_checker.check(word))
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/
H A Dfile.scala155 def check(file: JFile) { if (pred(file)) result += file }
157 if (start.isFile) check(start)
163 if (include_dirs) check(path.toFile)
168 check(path.toFile)
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Tools/
H A Dbuild_docker.scala91 echo = true).check
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/VSCode/src/
H A Dvscode_spell_checker.scala51 if (spell_checker.check(word))
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/
H A Djedit_spell_checker.scala60 if (spell_checker.check(word))
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/
H A Darm_encoderLib.sml89 fun check (f,m) b = (b () orelse raise ERR f (term_to_string m); I); function
91 fun check_is_15 s tm = check (s,tm) (fn _ => is_PC tm);
157 check ("encode_mode3", tm) (fn _ => width_okay 8 imm12)
160 check ("encode_mode3", tm) (fn _ => is_0 imm2)
233 check ("encode_branch", tm) (fn _ => is_T toarm orelse is_PC cond)
252 check ("encode_data_processing", tm) (fn _ => check_dp (opc,d,n))
383 check ("encode_load_store", tm) (fn _ => is_0 imm8)
387 check ("encode_load_store", tm) (fn _ => is_0 imm8)
422 check ("encode_miscellaneous", pairSyntax.mk_pair (cond,tm))
478 let val checkbr = check ("thumb_encode_branc
[all...]
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/regular-play/src/
H A DregexSemanticsScript.sml38 (* sanity check and helper lemmata *)
/seL4-l4v-10.1.1/HOL4/src/1/
H A DSanity.sig30 2 : no check
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86/
H A Dx86_Script.sml33 if EVERY (\x. ~(x = NONE)) (XREAD_INSTR_BYTES n e s) (* check that the memory is there *)
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/
H A Dx64_Script.sml33 if EVERY (\x. ~(x = NONE)) (ZREAD_INSTR_BYTES n e s) (* check that the memory is there *)
/seL4-l4v-10.1.1/HOL4/polyml/modules/IntInfAsInt/
H A DMakefile.in345 check-am: all-am
346 check: check-am
447 .PHONY: all all-am all-local check check-am clean clean-generic \
/seL4-l4v-10.1.1/HOL4/tools/Holmake/
H A Dinternal_functions.sml210 fun check s = function
217 case List.filter check files of
248 fun check p = function
262 smash (get_first check paths)
264 | NONE => if isUnix then "" else smash (check ".")
/seL4-l4v-10.1.1/graph-refine/
H A Dloop_bounds.py1 import check,search,problem,syntax,solver,logic,rep_graph,re namespace
4 from check import restr_others,split_visit_one_visit
196 checks = (check.single_loop_induct_step_checks (p, restrs, hyps, tag,
198 + check.single_loop_induct_base_checks (p, restrs, hyps, tag,
201 groups = check.proof_check_groups (checks)
203 (res, _) = check.test_hyp_group (rep, group)
518 hyp = check.mk_loop_counter_eq_hyp (p, split, restrs, n - 2)
563 checks = check.split_checks (p, (), hyps, split, tags = [asm_tag, c_tag])
564 groups = check.proof_check_groups (checks)
567 (res, el) = check
[all...]
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/include/
H A DMakefile.in475 check-am: all-am
476 check: check-am
581 .PHONY: CTAGS GTAGS TAGS all all-am check check-am clean clean-generic \
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/man/
H A DMakefile.in430 check-am: all-am
431 check: check-am
537 .PHONY: all all-am check check-am clean clean-generic clean-libtool \
/seL4-l4v-10.1.1/HOL4/src/HolQbf/
H A DQbfCertificate.sml163 (* check: proves or disproves the QBF 't' (see QDimacs.sml for the format of *)
178 fun check t dict (VALID (exts,lits)) = let function
352 Feedback.HOL_WARNING "QbfCertificate" "check" "final theorem has hyps"
356 Feedback.HOL_WARNING "QbfCertificate" "check"
362 | check t _ (INVALID (dict, cindex)) =
410 raise ERR "check"
414 raise ERR "check"
434 Feedback.HOL_WARNING "QbfCertificate" "check" "final theorem has hyps"
439 Feedback.HOL_WARNING "QbfCertificate" "check" "final theorem not F"

Completed in 329 milliseconds

1234567891011>>