/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/bytecode/ |
H A D | lisp_alt_semanticsScript.sml | 22 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 D | lisp_semanticsScript.sml | 169 (!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 D | lisp_extractScript.sml | 43 ``!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 D | stmonad.sig | 7 val ok : ('a, unit) stmonad value
|
H A D | optmonad.sml | 12 fun ok env = return () env function 43 fun repeatn' 0 f = ok 49 fun repeat p env = ((p >> repeat p) ++ ok) env
|
H A D | errormonad.sig | 10 val ok : ('a, unit, 'c) t value
|
H A D | stmonad.sml | 16 fun ok s = return () s function
|
H A D | errormonad.sml | 12 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 D | seqmonad.sml | 5 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 D | optmonad.sig | 8 val ok : ('a, unit) optmonad value
|
H A D | seqmonad.sig | 8 val ok : ('a, unit) seqmonad value
|
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/milawa-prover/ |
H A D | milawa_execScript.sml | 29 (!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 D | Makefile | 15 @grep -v 'HOL.* (built \|^\(- \)*runtime: \|User: ' <result.ok >$(TMPFILE1)
|
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/ |
H A D | Heap.h | 64 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 D | holdeptool.sml | 5 fun ok () = OS.Process.exit OS.Process.success function 25 | ["-h"] => usage ok
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/poly/ |
H A D | genscriptdep.sml | 32 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 D | lisp_opsScript.sml | 53 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 D | bddio.c | 384 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 D | cppext.cxx | 83 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 D | selftest.sml | 29 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 D | build_doc.scala | 48 if (res1.ok) { 58 if (res2.ok) {
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Admin/ |
H A D | build_doc.scala | 48 if (res1.ok) { 58 if (res2.ok) {
|
/seL4-l4v-10.1.1/HOL4/src/string/ |
H A D | selftest.sml | 71 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 D | process_result.scala | 23 def ok: Boolean = rc == 0
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/System/ |
H A D | process_result.scala | 23 def ok: Boolean = rc == 0
|