Searched refs:function (Results 226 - 250 of 876) sorted by relevance

1234567891011>>

/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DRule.sig59 val subtermsConv : conv -> conv (* All function arguments *)
175 val functionCongruence : Term.function -> Thm.thm
H A DAtom.sig50 (* A total comparison function for atoms. *)
H A DPortableMosml.sml54 (* Timing function applications. *)
/seL4-l4v-master/isabelle/src/Doc/Tutorial/document/
H A Dbasics.tex122 \item[function types,]\index{function types}
133 function.
154 applying functions to arguments. If \isa{f} is a function of type
175 \isa{\isasymlambda{}x.~x+1} is the function that takes an argument \isa{x} and
192 Equality\index{equality} is available in the form of the infix function
222 important overloaded function symbols.
231 Isabelle allows infix functions like \isa{+}. The prefix form of function
H A Dadvanced0.tex32 %proof time. In HOL you may have to work hard to define a function, but proofs
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DRule.sig59 val subtermsConv : conv -> conv (* All function arguments *)
175 val functionCongruence : Term.function -> Thm.thm
/seL4-l4v-master/l4v/isabelle/src/Doc/Tutorial/document/
H A Dbasics.tex122 \item[function types,]\index{function types}
133 function.
154 applying functions to arguments. If \isa{f} is a function of type
175 \isa{\isasymlambda{}x.~x+1} is the function that takes an argument \isa{x} and
192 Equality\index{equality} is available in the form of the infix function
222 important overloaded function symbols.
231 Isabelle allows infix functions like \isa{+}. The prefix form of function
/seL4-l4v-master/HOL4/examples/fun-op-sem/cbv-lc/
H A DtypesScript.sml26 (* Get the size function generated by the call to Datatype *)
56 (* Define a helper function for the termination argument below. *)
/seL4-l4v-master/HOL4/src/opentheory/reader/
H A DOpenTheoryReader.sig43 An axiom function for readers that tries to find the desired theorem in the
57 current theory. The first argument to [define_const_in_thy] is a function to
/seL4-l4v-master/HOL4/examples/fun-op-sem/small-step/
H A DdetermSemScript.sml24 * - a step function (to an option for representing stuckness),
59 * - a evaluation function
/seL4-l4v-master/HOL4/src/postkernel/
H A DTheory.sig81 already been stored. The set_theory_data function overrides whatever
127 (* Theory files (which are just SML source code) call this function as
/seL4-l4v-master/HOL4/src/compute/src/
H A Dcompute_rules.sml19 fun RULES_ERR function message =
21 origin_function = function,
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/X86Code/
H A DX86FOREIGNCALL.sml57 rbx, rbp, rdi, rsi, rsp, r12-r15 are saved by the called function.
59 ebx, edi, esi, ebp and esp are saved by the called function.
330 CallAddress(RegisterArg entryPtrReg), (* Call the function *)
338 (* Since this is an ML function we need to remove any ML stack arguments. *)
403 version we make this a function. *)
456 (* Build a foreign call function. The arguments are the abi, the list of argument types and the result type.
457 The result is the code of the ML function that takes three arguments: the C function to call, the arguments
484 | (CTypeVoid, _) => raise Foreign.Foreign "Void cannot be used for a function argument"
560 (* Adjustment to be made when the function return
[all...]
/seL4-l4v-master/isabelle/src/Doc/Logics/document/
H A DCTT.tex115 \index{*"` symbol}\index{function applications!in CTT}
119 \tt ` & $[i,i]\to i$ & Left 55 & function application\\
135 \rm function space $A\to B$ \\
170 the function application operator (sometimes called `apply'), and the 2-place
173 \hbox{\tt lam $x$. $b$} and $b{\tt`}a$. A CTT function~$f$ is simply an
424 it can even express Ackermann's function, which is not primitive recursive
428 include function types as a special case. The rules correspond to the
722 the predecessor function is $\lambda v. {\tt rec}(v, 0, \lambda x\,y. x)$.
757 predecessor function on the natural numbers.
799 $\prod@{x\in N}N$, which is shown as the function typ
[all...]
/seL4-l4v-master/l4v/isabelle/src/Doc/Logics/document/
H A DCTT.tex115 \index{*"` symbol}\index{function applications!in CTT}
119 \tt ` & $[i,i]\to i$ & Left 55 & function application\\
135 \rm function space $A\to B$ \\
170 the function application operator (sometimes called `apply'), and the 2-place
173 \hbox{\tt lam $x$. $b$} and $b{\tt`}a$. A CTT function~$f$ is simply an
424 it can even express Ackermann's function, which is not primitive recursive
428 include function types as a special case. The rules correspond to the
722 the predecessor function is $\lambda v. {\tt rec}(v, 0, \lambda x\,y. x)$.
757 predecessor function on the natural numbers.
799 $\prod@{x\in N}N$, which is shown as the function typ
[all...]
/seL4-l4v-master/HOL4/examples/dev/sw2/test/
H A DregAllocTest.sml10 (* Test case 1: The factorial function. *)
/seL4-l4v-master/HOL4/src/0/
H A DSubst.sml85 * Composition of 2 substitution. We need to provide a function [mk_cl] that
/seL4-l4v-master/HOL4/src/compute/examples/
H A DArith.sml40 * function strongly.
/seL4-l4v-master/HOL4/src/datatype/mutrec/examples/
H A Dvar_example.sml75 (* A simple function for finding the variables in a program *)
/seL4-l4v-master/HOL4/src/metis/
H A DmlibMultiset.sml72 prevents this function being implemented :-(
/seL4-l4v-master/HOL4/developers/mlton-srcs/
H A DBinarymap.sml50 [app f m] applies function f to the entries (k, v) in m, in
54 [revapp f m] applies function f to the entries (k, v) in m, in
57 [foldl f e m] applies the folding function f to the entries (k, v)
60 [foldr f e m] applies the folding function f to the entries (k, v)
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/
H A DCOMPILERBODYSIG.sml59 Returns the parse tree and, if successful, a function that executes the
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/
H A DBaseParseTreeSig.sml220 (* A function binding is a list of clauses, each of which uses a
221 valBinding to hold the list of patterns and the corresponding function
222 body. The second pass extracts the function variable and the number of
235 and fvalclause = (* Clause within a function binding. *)
/seL4-l4v-master/HOL4/polyml/basis/
H A DOption.sml21 (* G&R 2004 status: updated, added "app" function. *)
H A DRealArray.sml26 function to load and store reals although it would probably be

Completed in 256 milliseconds

1234567891011>>