Searched refs:check (Results 76 - 100 of 382) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/polyml/modules/
H A DMakefile.in118 RECURSIVE_TARGETS = all-recursive check-recursive cscopelist-recursive \
524 check-am: all-am
525 check: check-recursive
627 .PHONY: $(am__recursive_targets) CTAGS GTAGS TAGS all all-am check \
628 check-am clean clean-generic clean-libtool cscopelist-am ctags \
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmlibTermorder.sml182 (* A partial order on equations, designed to be quick to check. *)
419 fun check eqns = function
426 (* Uncomment this check function to print out the linear arithmetic problems
433 val check = fn eqns =>
435 val (t,r) = timed check eqns
451 if inconsistent (check (omega_eqns vars eqns)) then NONE
H A DmlibSolver.sml218 fun schedule check slice read stat =
222 if not (check ()) then
261 fun check () = check_meter (!slice) function
269 fn goal => schedule check slce read stat (map (C init_subnode goal) cnodes)
/seL4-l4v-10.1.1/isabelle/src/Pure/System/
H A Disabelle_system.scala53 if (_settings.isEmpty) init() // unsynchronized check
161 bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check
312 try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") }
321 def hostname(): String = bash("hostname -s").check.out
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/System/
H A Disabelle_system.scala53 if (_settings.isEmpty) init() // unsynchronized check
161 bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check
312 try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") }
321 def hostname(): String = bash("hostname -s").check.out
/seL4-l4v-10.1.1/HOL4/src/res_quan/src/
H A Dres_quanLib.sml348 (* check st l : Fail with st if l is empty, otherwise return l. *)
351 local fun check st l = if null l then raise ERR "check" st else l function
386 val imps = check "RESQ_RES_THEN: no restricted quantification " ths
388 val res = check "RESQ_RES_THEN: no resolvents " l
389 val tacs = check "RESQ_RES_THEN: no tactics" (mapfilter ttac res)
478 (* check that tm is a <varstruct> where:
500 (* check that tm is a <lhs> where:
/seL4-l4v-10.1.1/HOL4/tools/Holmake/
H A Dparse_glob.sml109 fun check s = function
127 grab_word classnames >- check
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/translations/
H A DtranslationsLib.sig46 * These functions translate some ltl problems to an check whether there is
61 * These functions translate some ltl problems to an check whether there is
/seL4-l4v-10.1.1/isabelle/src/Pure/PIDE/
H A Dresources.scala40 def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None
44 if (path.is_absolute || path.is_current) check(path)
46 check(Path.explode("~~/src/Pure") + path) orElse
48 else check(Path.explode("$ML_SOURCES") + path))
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DModel.sig230 (* Note: if it's cheaper, a systematic check will be performed instead. *)
233 val check : value
H A DWaiting.sml117 fun check ((parm,model),z) = function
121 val {T,F} = Model.check Model.interpretClause n model fv cl
126 List.foldl check 1.0 (zip parms models)
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/PIDE/
H A Dresources.scala40 def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None
44 if (path.is_absolute || path.is_current) check(path)
46 check(Path.explode("~~/src/Pure") + path) orElse
48 else check(Path.explode("$ML_SOURCES") + path))
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DModel.sig230 (* Note: if it's cheaper, a systematic check will be performed instead. *)
233 val check : value
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/
H A Dregexp2dfa.sml327 fun check(J,lstring,name,string) = function
333 of ["-dfagen","SML",lstring,name,string] => check(regexpLib.SML,lstring,name,string)
334 | ["-dfagen","HOL",lstring,name,string] => check(regexpLib.HOL,lstring,name,string)
335 | [lstring,name,string] => check(justifyDefault, lstring, name,string)
/seL4-l4v-10.1.1/HOL4/src/HolQbf/
H A Dselftest.sml10 (* check whether Squolem is installed *)
/seL4-l4v-10.1.1/HOL4/src/tfl/src/
H A Dselftest.sml12 (* check parsability of quantified equation *)
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86/
H A Dx86_astScript.sml28 (* check whether rm requires a lock, i.e. specifies a memory access *)
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/
H A Dx64_astScript.sml25 (* check whether rm requires a lock, i.e. specifies a memory access *)
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/
H A Dpolystring.cpp154 int check = WideCharToMultiByte(codePage, 0, buffer, (int)buffLen, result->chars, outputLen, NULL, NULL); local
155 if (check <= 0) return EmptyString(mdTaskData);
/seL4-l4v-10.1.1/HOL4/src/integer/
H A DintSimps.sml251 fun check tm = function
254 RCACHE (dpvars,check,CTXT_ARITH DP DPname)
255 (* the check function determines whether or not a term might be handled
/seL4-l4v-10.1.1/HOL4/src/portableML/
H A DUTF8.sml114 check acc (pos + 1) pos (bc - 1)
117 and check acc pos start cnt = value
124 if isCont_char c then check acc (pos + 1) start (cnt - 1)
/seL4-l4v-10.1.1/HOL4/tools/
H A Dconfigure-mosml.sml107 fun check p = function
123 findpartial check paths
125 | NONE => if OS = "winNT" then check "." else NONE
/seL4-l4v-10.1.1/HOL4/tools-poly/
H A Dsmart-configure.sml137 fun check p = function
153 findpartial check paths
155 | NONE => if OS = "winNT" then check "." else NONE
/seL4-l4v-10.1.1/graph-refine/
H A Dsearch.py11 import check namespace
12 from check import restr_others, loops_to_split, ProofNode
57 init_hyps = check.init_point_hyps (p)
87 def check (i): function in function:find_split_limit
106 map (check, check_order)
109 check (split)
742 hyps = check.init_point_hyps (p)
828 (r_start, r_step), 'Seq check failed'))
870 hyps = hyps + [check.non_r_err_pc_hyp (tags,
1187 hyp = check
[all...]
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/model/
H A Dx64AssemblerLib.sml190 fun check false _ _ = NONE function
191 | check true l s =
204 | [(bs, s)] => (s, SOME (bs, check c l s))

Completed in 585 milliseconds

1234567891011>>