Searched refs:exp (Results 151 - 175 of 228) sorted by relevance

12345678910

/seL4-l4v-master/HOL4/examples/dev/sw/
H A DannotatedIR.sml21 type annt = {fspec : thm, ins : exp, outs : exp, context : exp list};
24 type cond = exp * rop * exp;
H A DfunCall.sml204 | one_arg (exp, (invRegLs, i)) =
205 (isBroken := true; (([exp],false, i) :: invRegLs, i-1))
408 List.map (fn exp => ( i := !i + 1; MEM(11, ~(3 + (len - !i))))) expL
H A DpreARMScript.sml182 read (regs,mem) (exp:EXP) =
183 case exp of
206 write (regs,mem) (exp:EXP) (v:DATA)=
207 case exp of
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/
H A DannotatedIR.sml12 type annt = {fspec : thm, ins : exp, outs : exp, context : exp list};
15 type cond = exp * rop * exp;
H A DfunCall.sml192 | one_arg (exp, (invRegLs, i)) =
193 (isBroken := true; (([exp],false, i) :: invRegLs, i-1))
396 List.map (fn exp => ( i := !i + 1; MEM(11, ~(3 + (len - !i))))) expL
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/
H A DannotatedIR.sml12 type annt = {fspec : thm, ins : exp, outs : exp, context : exp list};
15 type cond = exp * rop * exp;
H A DfunCall.sml189 | one_arg (exp, (invRegLs, i)) =
190 (isBroken := true; (([exp],false, i) :: invRegLs, i-1))
393 List.map (fn exp => ( i := !i + 1; MEM(11, ~(3 + (len - !i))))) expL
/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A Dselftest.sml872 val cl = LS[`exp $x 0 = 1`];
874 val cl = LS[`$y = 0`,`exp $x $y = $x * exp $x (pre $y)`];
1035 and expFnName = Name.fromString "exp"
1064 `$y <= exp $x`]);
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/extract/
H A Dlisp_extractScript.sml420 ``!fns2 io io2 args a fc fns params exp x ok2 res.
421 fc IN FDOM fns /\ (fns ' fc = (params,exp)) /\
423 R_ev (exp,VarBind params args,fns,io,ok) res ==>
430 (b ==> R_ap (Fun name,args,e,k,io,ok) exp) ==>
433 ((ok ==> b) ==> R_ap (Fun name,args,e,k,io,ok) (if ok then exp else (Sym "NIL",k,io,ok)))``,
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A Dselftest.sml872 val cl = LS[`exp $x 0 = 1`];
874 val cl = LS[`$y = 0`,`exp $x $y = $x * exp $x (pre $y)`];
1035 and expFnName = Name.fromString "exp"
1064 `$y <= exp $x`]);
/seL4-l4v-master/HOL4/examples/algebra/polynomial/
H A DpolyBinomialScript.sml322 ((PolyRing r).prod.exp (x + y) 2 =
323 (PolyRing r).prod.exp x 2 +
324 (PolyRing r).sum.exp |1| 2 * (x * y) +
325 (PolyRing r).prod.exp y 2) : thm
332 ((PolyRing r).prod.exp (p + q) 2 =
333 (PolyRing r).prod.exp p 2 +
334 (PolyRing r).sum.exp |1| 2 * (p * q) +
335 (PolyRing r).prod.exp q 2) : thm
337 val _ = overload_on ("**", ``(PolyRing r).prod.exp``);
344 p ** 2 + (PolyRing r).sum.exp |
[all...]
/seL4-l4v-master/HOL4/src/tfl/src/
H A DDefn.sml1592 fun exp (AQ(locn,tm)) S = function
1594 | exp (IDENT (p as (locn,s))) S =
1598 | exp (QIDENT (p as (locn,s,_))) S =
1600 then raise ERRloc "exp" locn "wildcard in long id. in pattern"
1602 | exp (APP(locn,M,N)) S =
1603 let val (M',S') = exp M S
1604 val (N', S'') = exp N S'
1607 | exp (TYPED(locn,M,pty)) S =
1608 let val (M',S') = exp M S in (TYPED(locn,M',pty),S') end
1609 | exp (LA
[all...]
/seL4-l4v-master/HOL4/src/probability/
H A DderivativeScript.sml1894 ``!z. ((\n. z pow n / (&(FACT n))) sums exp(z)) (from 0)``,
1895 SIMP_TAC std_ss [exp] THEN
1909 ``!w z. ((\n. z pow n / (&(FACT n))) sums w) (from 0) <=> (w = exp(z))``,
1917 ==> abs(sum((0:num)..n) (\i. z pow i / (&(FACT i))) - exp(z)) <= e``,
1939 ``!z. (exp has_derivative (\y. exp z * y)) (at z)``,
1944 `exp:real->real`, `from (0)`]
1958 exp x) <= e) /\
1994 MAP_EVERY Q.EXISTS_TAC [`(&0)`, `exp((&0))`] THEN
2034 ``!z. exp continuou
[all...]
/seL4-l4v-master/HOL4/examples/elliptic/
H A DfieldTools.sml641 val (exp,varmap) = field_to_exp tm [] value
657 val exp = Algebra.normalize {equations = eqns} exp value
659 val tm' = exp_to_field field varmap exp
/seL4-l4v-master/HOL4/src/integer/
H A DOmegaMath.sml1087 relations of the form d | exp where exp includes at least one
1118 relations of the form ~(d | exp) where exp includes at least one
H A DintSyntax.sml91 val dest_exp = dest_binop exp_tm ("dest_exp", "Term not an exp")
/seL4-l4v-master/HOL4/src/n-bit/
H A DblastLib.sml244 mk_summation : returns theorems of the form ``BSUM i x y c = exp``
245 for all 0 < i < max, where "exp" is a propositional
307 mk_carry : returns theorem of the form ``BCARRY max x y c = exp``,
308 where "exp" is a propositional expression.
/seL4-l4v-master/HOL4/examples/separationLogic/src/holfoot/
H A Dholfoot_pp_print.sml675 (fn (tag,exp) =>
678 sys (Top, Top, Top) (d - 1) exp
696 (fn (tag,exp) =>
699 sys (Top, Top, Top) (d - 1) exp
/seL4-l4v-master/HOL4/examples/algebra/field/
H A DfieldInstancesScript.sml500 ((GF n).sum.exp 1 n = 0) /\
501 !m. 0 < m /\ m < n ==> (GF n).sum.exp 1 m <> 0
535 `((GF n).sum.exp 1 n = 0) /\ !m. 0 < m /\ m < n ==> (GF n).sum.exp 1 m <> 0` suffices_by metis_tac[finite_ring_char_alt] >>
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/
H A DBaseCodeTreeSig.sml107 | Handle of (* Exception handler. *) { exp: codetree, handler: codetree, exPacketAddr: int }
H A DBackendIntermediateCodeSig.sml75 | BICHandle of (* Exception handler. *) { exp: backendIC, handler: backendIC, exPacketAddr: int }
/seL4-l4v-master/HOL4/polyml/libpolyml/
H A Dexporter.cpp576 ExportRequest(Handle root, Exporter *exp): MainThreadRequest(MTP_EXPORTING), argument
577 exportRoot(root), exporter(exp) {}
/seL4-l4v-master/HOL4/examples/algebra/finitefield/
H A DffConjugateScript.sml897 Hence order r.prod (f*.exp x (CARD B ** n)) * (gcd a (CARD B ** n)) = a by group_order_power
1467 ZN_exp |- !n. 0 < n ==> !x k. (ZN n).prod.exp x k = x ** k MOD n
1551 !n m. n < forder x /\ m < forder x /\ (f*.exp x n = f*.exp x m) ==> (n = m):
1554 !x. x IN g.carrier ==> !n m. n < order g x /\ m < order g x /\ ((g.exp x n = (g.exp x m) ==> (n = m): thm
1584 Note f*.exp = $** by field_nonzero_mult_property
1601 Note !x k. g.exp x k = (ZN ox).prod.exp x k by Invertibles_property
1602 and !x k. (ZN ox).prod.exp
[all...]
/seL4-l4v-master/HOL4/examples/dev/
H A Dcompile.sig146 (* CompileExp exp *)
148 (* [REC assumption] |- <circuit> ===> DEV exp *)
/seL4-l4v-master/HOL4/src/metis/
H A DmlibModel.sml126 | func ("exp",[m,n]) = SOME (funpow n (fn x => f (x * m)) one)
156 | func ("exp",[m,n]) = SOME (funpow n (fn x => f (x * m)) one)

Completed in 252 milliseconds

12345678910