Searched refs:ok (Results 51 - 75 of 140) sorted by relevance

123456

/seL4-l4v-master/HOL4/examples/theorem-prover/milawa-prover/
H A Dmilawa_proofpScript.sml2519 !x1 x2 x3 x4 io ok. ?res ok2 io2.
2520 R_ap (Fun name,[x1;x2;x3;x4],ARB,k,io,ok) (res,k,io ++ io2,ok2) /\
2533 \\ Q.EXISTS_TAC `logic_proofp x1 x2 x3 x4` \\ Q.EXISTS_TAC `ok`
2605 let (f,args,env,k,io,ok) = x in
2608 R_ap (f,args,env,add_def k d,io,ok) (res,add_def k2 d,io2,ok2)) /\
2610 let (e,env,k,io,ok) = x in
2613 R_evl (e,env,add_def k d,io,ok) (res,add_def k2 d,io2,ok2)) /\
2615 let (e,env,k,io,ok) = x in
2618 R_ev (e,env,add_def k d,io,ok) (res,add_def k2 d,io2,ok2))``,
2632 ``R_ap (f,args,env,k,io,ok) (re
[all...]
/seL4-l4v-master/HOL4/examples/formal-languages/regular/regular-play/src/
H A DregexSemanticsScript.sml65 (* ok, but not quite all - just 2 *)
/seL4-l4v-master/HOL4/examples/formal-languages/context-free/
H A DgrammarLib.sml13 fun ok e = return () e function
43 fun repeat (m : 'a tt) s = ((m >> repeat m) ++ ok) s
151 fun dropP P = repeat (getc "" >- (fn c => if P c then ok
161 if i = sz then ok
178 | Error _ => ok s
209 fun lex m = repeat ((getP Char.isSpace >> ok) ++ comment) >> m
210 fun complete m = m <- repeat ((getP Char.isSpace >> ok) ++ comment)
/seL4-l4v-master/HOL4/src/portableML/poly/concurrent/
H A DFuture.sml193 val ok = value
196 foldl' (fn job => fn ok => job valid andalso ok) jobs true) ());
207 if ok andalso not (Exn.is_interrupt_exn test) then ()
382 val ok = value
387 in ok end;
395 fun job ok =
398 if ok then
598 fun job ok =
599 assign_result group result (if ok the
[all...]
/seL4-l4v-master/HOL4/src/simp/src/
H A DCache.sml45 fun ok (prev,SOME thm) = prev << curr function
46 | ok (prev,NONE) = curr << prev
48 (case snd (first ok prevs) of
223 fun ok (cached, SOME _) = cached << hyps function
224 | ok (cached, NONE) = hyps << cached
226 case List.find ok cache_F of
/seL4-l4v-master/HOL4/src/parse/
H A Dqbuf.sml132 val (buffered, ok) =
140 if ok then
H A DPretype.sml73 UVar j => if i = j then ok
85 if v1 = v2 then ok
98 and unifyl [] [] = ok
/seL4-l4v-master/isabelle/src/Pure/General/
H A Dcompletion.scala434 val ok =
437 if (ok) Some((abbr, abbrevs))
464 ok =
467 if ok
/seL4-l4v-master/l4v/isabelle/src/Pure/General/
H A Dcompletion.scala434 val ok =
437 if (ok) Some((abbr, abbrevs))
464 ok =
467 if ok
/seL4-l4v-master/isabelle/src/Tools/VSCode/src/
H A Dserver.scala276 if (!build(no_build = true).ok) {
283 if (!build().ok) { progress.echo(fail_msg); error(fail_msg) }
314 case Session.Terminated(result) if !result.ok =>
345 if (result.ok) reply("") else reply("Prover shutdown failed: return code " + result.rc)
/seL4-l4v-master/l4v/isabelle/src/Tools/VSCode/src/
H A Dserver.scala276 if (!build(no_build = true).ok) {
283 if (!build().ok) { progress.echo(fail_msg); error(fail_msg) }
314 case Session.Terminated(result) if !result.ok =>
345 if (result.ok) reply("") else reply("Prover shutdown failed: return code " + result.rc)
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/model/
H A DarmAssemblerLib.sml50 fun ok r = (Portable.inc pc; mlibUseful.INR r) function
73 then ok w :: p1
77 ( addWarning s1; ok w :: p1 ))
86 | WORD w => ok w :: p1
/seL4-l4v-master/HOL4/examples/l3-machine-code/m0/model/
H A Dm0AssemblerLib.sml51 fun ok e r = (incpc e; mlibUseful.INR r) function
80 Thumb16 w => ok Enc_Narrow w :: p1
82 ok Enc_Wide (BitsN.@@ (w1, w2)) :: p1
95 | HALFWORD w => ok Enc_Narrow w :: p1
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/bytecode/
H A Dlisp_compilerScript.sml33 ok : bool |>`;
81 BC_FAIL bc = bc with ok := F`;
675 ~bc.ok ==>
715 ``(BC_ADD_CONST bc s).ok = bc.ok``,
725 (bc2.ok = bc.ok) /\
733 (bc2.ok = bc.ok) /\
741 (bc2.ok
[all...]
/seL4-l4v-master/isabelle/src/Tools/jEdit/src/
H A Dpretty_text_area.scala211 val (pattern, ok) =
223 if (ok) search_field_foreground
/seL4-l4v-master/l4v/isabelle/src/Tools/jEdit/src/
H A Dpretty_text_area.scala211 val (pattern, ok) =
223 if (ok) search_field_foreground
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm8/model/
H A Darm8AssemblerLib.sml75 fun ok r = (Portable.inc pc; mlibUseful.INR r) function
97 then ok w :: p1
102 | WORD w => ok w :: p1
/seL4-l4v-master/HOL4/examples/l3-machine-code/x64/model/
H A Dx64AssemblerLib.sml40 fun ok l = (incpc (List.length l); mlibUseful.INR l) function
58 | l => ok l :: p1)
64 | STREAM l => ok l :: p1
/seL4-l4v-master/HOL4/examples/elliptic/
H A DsubtypeTools.sml208 val (ok,eq) = cmp (a,b) value
210 (if ok then ALL_CONV else comm_conv solver) THENC
215 val (ok,eq) = cmp (a,b) value
217 (if ok then ALL_CONV else comm_conv' solver) THENC
219 (if ok then ALL_CONV else push_conv' solver))
/seL4-l4v-master/HOL4/tools/Holmake/
H A DHolmake_types.sml133 val (ok, spaces) = splitr Char.isSpace ss value
134 val (ok0, bslashes) = splitr (fn c => c = #"\\") ok
136 if size bslashes mod 2 = 0 then ok
138 slice(ss, 0, SOME (size ok + 1))
139 else ok
H A Dinternal_functions.sml59 val (ok, rest) = position (string from) ss value
62 recurse (to::ok::acc) (slice(rest, size from, NONE))
63 else concat (List.rev (ok::acc))
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/extract/
H A Dlisp_extractLib.sml397 val lemma = DISCH_ALL (ASSUME ``R_ap (Fun ^name_tm,args,e,fns,io,ok) (^v args,fns,io,ok)``)
402 val th2 = CS [R_ap_Fun] ``R_ap (Fun ^name_tm,^args,e,k,io,ok) (ans,k2,io2,ok2)``
461 val lemma = DISCH_ALL (ASSUME ``R_ap (Fun ^name_tm,args,e,fns,io,ok) (^v args,fns,io,ok)``)
469 val th2 = CS [R_ap_Fun] ``R_ap (Fun ^name_tm,^args,e,k,io,ok) (ans,k2,io2,ok2)``
731 val lemma = DISCH_ALL (ASSUME ``R_ap (Fun ^name_tm,args,e,fns,io,ok) (^v (args,fns,io,ok))``)
732 |> DISCH ``^v2 (args,fns,io,ok)`` |> PURE_REWRITE_RULE [AND_IMP_INTRO]
738 val th2 = CS [R_ap_Fun] ``R_ap (Fun ^name_tm,^args,e,k,io,ok) re
[all...]
/seL4-l4v-master/isabelle/src/Pure/Tools/
H A Dphabricator.scala165 if (!result.ok) error("Return code: " + result.rc.toString)
279 if (!Isabelle_System.bash("mkdir -p " + File.bash_path(root_path)).ok) {
314 if (!Isabelle_System.bash("mkdir -p " + File.bash_path(repo_path)).ok) {
897 def ok: Boolean = error.isEmpty
898 def get: JSON.T = if (ok) result else Exn.error(error.get)
/seL4-l4v-master/l4v/isabelle/src/Pure/Tools/
H A Dphabricator.scala165 if (!result.ok) error("Return code: " + result.rc.toString)
279 if (!Isabelle_System.bash("mkdir -p " + File.bash_path(root_path)).ok) {
314 if (!Isabelle_System.bash("mkdir -p " + File.bash_path(repo_path)).ok) {
897 def ok: Boolean = error.isEmpty
898 def get: JSON.T = if (ok) result else Exn.error(error.get)
/seL4-l4v-master/HOL4/tools/Holmake/poly/
H A DBuildCommand.sml339 (* incinfos not consulted for comparison so empty value ok here *)
444 fun interpret_graph (g,ok) =
445 (if ok then OS.Process.success else OS.Process.failure, g)

Completed in 302 milliseconds

123456