Searched refs:ok (Results 1 - 25 of 130) sorted by relevance

123456

/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/bytecode/
H A Dlisp_alt_semanticsScript.sml22 RR_ev (Const s, a,fns,io,ok) (s,fns,io,ok))
26 RR_ev (Var x,a,fns,io,ok) (a ' x,fns,io,ok))
29 RR_ev (Const (Sym "NIL"),a,fns,io,ok) (s,fns1,io1,ok1) ==>
30 RR_ev (Or [],a,fns,io,ok) (s,fns1,io1,ok1))
33 RR_ev (t,a,fns,io,ok) (s1,fns1,io1,ok1) /\ isTrue s1 ==>
34 RR_ev (Or (t::ts),a,fns,io,ok) (s1,fns1,io1,ok1))
37 RR_ev (t,a,fns,io,ok) (s1,fns1,io1,ok1) /\ ~(isTrue s1) /\
39 RR_ev (Or (t::ts),a,fns,io,ok) (s
[all...]
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/spec/
H A Dlisp_semanticsScript.sml169 (!s a fns io ok.
170 R_ev (Const s, a,fns,io,ok) (s,fns,io,ok))
172 (!x (a: string |-> SExp) fns io ok.
174 R_ev (Var x,a,fns,io,ok) (a ' x,fns,io,ok))
176 (!a fns io ok s fns1 io1 ok1.
177 R_ev (Const (Sym "NIL"),a,fns,io,ok) (s,fns1,io1,ok1) ==>
178 R_ev (Or [],a,fns,io,ok) (s,fns1,io1,ok1))
180 (!a fns io s1 fns1 io1 t ts ok
[all...]
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/extract/
H A Dlisp_extractScript.sml43 ``!x. x IN FDOM e ==> R_ev (Var x,e,fns,io,ok) (e ' x,fns,io,ok)``,
47 ``!x. T ==> R_ev (Const x,e,fns,io,ok) (x,fns,io,ok)``,
53 (bx ==> R_ev (x,e,fns,io,ok) (ans1,fns1,io1,ok1)) ==>
55 R_ev (If x y z,e,fns,io,ok)
66 (bx ==> R_ev (x,e,fns,io,ok) (ans1,fns1,io1,ok1)) ==>
68 R_ev (If x y z,e,fns,io,ok)
77 (bx ==> R_ev (x,e,fns,io,ok) (ans1,fns1,io1,ok1)) ==>
79 R_ev (Or (x::y::xs),e,fns,io,ok)
[all...]
/seL4-l4v-10.1.1/HOL4/src/portableML/monads/
H A Dstmonad.sig7 val ok : ('a, unit) stmonad value
H A Doptmonad.sml12 fun ok env = return () env function
43 fun repeatn' 0 f = ok
49 fun repeat p env = ((p >> repeat p) ++ ok) env
H A Derrormonad.sig10 val ok : ('a, unit, 'c) t value
H A Dstmonad.sml16 fun ok s = return () s function
H A Derrormonad.sml12 fun ok e = return () e (* eta-expanded b/c of value restriction *) function
41 fun repeatn' 0 f = ok
48 fun repeat p env = ((p >> repeat p) ++ ok) env
H A Dseqmonad.sml5 fun ok env = seq.result (env, ()) function
50 fun repeatn' 0 f = ok
56 fun repeat p env = ((p >> repeat p) ++ ok) env
H A Doptmonad.sig8 val ok : ('a, unit) optmonad value
H A Dseqmonad.sig8 val ok : ('a, unit) seqmonad value
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/milawa-prover/
H A Dmilawa_execScript.sml29 (!s a fns ok.
30 MR_ev (Const s,a,ctxt:context_type,fns,ok) (s,ok))
32 (!x (a: string |-> SExp) fns ok.
34 MR_ev (Var x,a,ctxt,fns,ok) (FAPPLY a x,ok))
36 (!a fns ok s ok1.
37 MR_ev (Const (Sym "NIL"),a,ctxt,fns,ok) (s,ok1) ==>
38 MR_ev (Or [],a,ctxt,fns,ok) (s,ok1))
40 (!a fns s1 t ts ok
[all...]
/seL4-l4v-10.1.1/HOL4/src/Boolify/test/
H A DMakefile15 @grep -v 'HOL.* (built \|^\(- \)*runtime: \|User: ' <result.ok >$(TMPFILE1)
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/
H A DHeap.h64 bool ok(int n) { return n >= 0 && n < (int)indices.size(); }
70 bool inHeap (int n) { assert(ok(n)); return indices[n] != 0; }
71 void increase (int n) { assert(ok(n)); assert(inHeap(n)); percolateUp(indices[n]); }
75 assert(ok(n));
/seL4-l4v-10.1.1/HOL4/tools/Holmake/
H A Dholdeptool.sml5 fun ok () = OS.Process.exit OS.Process.success function
25 | ["-h"] => usage ok
/seL4-l4v-10.1.1/HOL4/tools/Holmake/poly/
H A Dgenscriptdep.sml32 fun usage ok =
34 val strm = if ok then TextIO.stdOut else TextIO.stdErr
37 Process.exit (if ok then Process.success else Process.failure)
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/implementation/
H A Dlisp_opsScript.sml53 zLISP_ALT side (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) =
60 cond (lisp_inv (a1,a2,sl,sl1,e,ex,cs,ok) (x0,x1,x2,x3,x4,x5,^VAR_REST)
65 zLISP_R (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) =
72 cond (lisp_inv (a1,a2,sl,sl1,e,ex,cs,ok) (x0,x1,x2,x3,x4,x5,^VAR_REST)
87 ``zLISP (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok)``
295 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. tw2 = r2) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
296 val post_tm = ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,p+3w::qs,code,amnt,ok) * zPC r2``
305 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. tw2 = r2) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
306 val post_tm = ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,r2::qs,code,amnt,ok) * zPC (p+2w)``
315 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zP
[all...]
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/
H A Dbddio.c384 int ok; local
389 ok = bdd_save(ofile, r);
391 return ok;
478 int ok; local
483 ok = bdd_load(ifile, root);
485 return ok;
H A Dcppext.cxx83 int ok = bdd_init(n,c); local
88 return ok;
424 int ok, first; local
460 ok=1;
462 for (i=0 ; i<binsize && ok ; i++)
464 ok = 0;
467 ok = 0;
469 if (ok)
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/
H A Dselftest.sml29 val ok = snd ((holfootLib.holfoot_interactive_verify_spec (not quiet) (not quiet) (concat [examples_dir, file]) (SOME [generate_vcs]) [])); value
31 val _ = if (not ok andalso hard_fail) then Process.exit Process.failure else ();
32 in ok end
/seL4-l4v-10.1.1/isabelle/src/Pure/Admin/
H A Dbuild_doc.scala48 if (res1.ok) {
58 if (res2.ok) {
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Admin/
H A Dbuild_doc.scala48 if (res1.ok) {
58 if (res2.ok) {
/seL4-l4v-10.1.1/HOL4/src/string/
H A Dselftest.sml71 val (actual, ok) = let
77 if ok then OK() else die ("FAILED!\n Got "^actual)
/seL4-l4v-10.1.1/isabelle/src/Pure/System/
H A Dprocess_result.scala23 def ok: Boolean = rc == 0
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/System/
H A Dprocess_result.scala23 def ok: Boolean = rc == 0

Completed in 185 milliseconds

123456