Searched refs:function (Results 251 - 275 of 876) sorted by relevance

<<11121314151617181920>>

/seL4-l4v-master/HOL4/examples/misc/
H A DcontMonadScript.sml8 don't need to hide the function under a constructor, but this does
/seL4-l4v-master/HOL4/examples/muddy/
H A Dbvec.sig55 relates to C types and function declarations in bvec.h:
/seL4-l4v-master/isabelle/src/HOL/Hahn_Banach/document/
H A Droot.tex47 supremum (w.r.t.\ the function order) and extension of non-maximal functions.
/seL4-l4v-master/isabelle/src/HOL/Statespace/document/
H A Droot.tex45 spaces. The state is represented as a function from (abstract) names
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DAtom.sig50 (* A total comparison function for atoms. *)
H A DPortableMosml.sml54 (* Timing function applications. *)
/seL4-l4v-master/l4v/isabelle/src/Doc/Tutorial/document/
H A Dadvanced0.tex32 %proof time. In HOL you may have to work hard to define a function, but proofs
H A Dfp.tex146 \isa{x $\in$ set xs}, where \isa{set} is a function that turns a list into the
171 primitive recursive function definitions.
175 comes equipped with a \isa{size} function from $t$ into the natural numbers
270 \isacommand{primrec} function definition is turned into a proper
288 datatypes, including those involving function spaces, are covered in
291 form of recursive function definition that goes well beyond
388 involving function spaces is permitted: the recursive type may occur on the
389 right of a function arrow, but never on the left. Hence the above can of worms
397 If you need nested recursion on the left of a function arrow, there are
422 update function, an
[all...]
/seL4-l4v-master/l4v/isabelle/src/HOL/Hahn_Banach/document/
H A Droot.tex47 supremum (w.r.t.\ the function order) and extension of non-maximal functions.
/seL4-l4v-master/l4v/isabelle/src/HOL/Statespace/document/
H A Droot.tex45 spaces. The state is represented as a function from (abstract) names
/seL4-l4v-master/HOL4/examples/bootstrap/
H A Dsource_valuesScript.sml13 (* Since strings are not in the representation, we have a function that
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/
H A DBASE_PARSE_TREE.sml217 (* A function binding is a list of clauses, each of which uses a
218 valBinding to hold the list of patterns and the corresponding function
219 body. The second pass extracts the function variable and the number of
232 and fvalclause = (* Clause within a function binding. *)
/seL4-l4v-master/HOL4/polyml/basis/
H A DThreadLib.sml25 (* This applies a function while a mutex is being held.
H A DVectorOperations.sml51 (* Apply a function to each element in turn *)
72 (* Fold a function over a array. *)
115 (* Apply a function to each element in turn and update the array with the
H A DThread.sml35 There is no join function to wait for the completion of a thread.
40 using the interrupt function. This causes an interrupt to be
130 the function argument. The attribute list gives initial values for thread attributes
132 default values. The thread is terminated when the thread function returns, if
138 (*!Test if a thread is still running or has terminated. This function should be
238 If the thread is handling interrupts synchronously this function can be interrupted
239 using the `Thread.interrupt` function or, if the thread is set to
244 is signalled the function will return normally even if it has not yet re-acquired
248 A thread should never call this function if it may receive an asynchronous
280 open Thread (* Created in INITIALISE with thread type and self function
[all...]
/seL4-l4v-master/HOL4/Manual/Description/
H A Dsyntax.tex39 & | & \type\ \verb+->+\ \type & \mbox{(function arrow)} \\
52 function types; it can be written with an infix arrow. The nullary
60 are both well-formed types. The function arrow is ``right associative'',
/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/
H A Dsyntax.tex39 & | & \type\ \verb+->+\ \type & \mbox{(function arrow)} \\
52 function types; it can be written with an infix arrow. The nullary
60 are both well-formed types. The function arrow is "right associative",
/seL4-l4v-master/isabelle/src/Doc/Tutorial/document/
H A Dfp.tex146 \isa{x $\in$ set xs}, where \isa{set} is a function that turns a list into the
171 primitive recursive function definitions.
175 comes equipped with a \isa{size} function from $t$ into the natural numbers
270 \isacommand{primrec} function definition is turned into a proper
288 datatypes, including those involving function spaces, are covered in
291 form of recursive function definition that goes well beyond
388 involving function spaces is permitted: the recursive type may occur on the
389 right of a function arrow, but never on the left. Hence the above can of worms
397 If you need nested recursion on the left of a function arrow, there are
422 update function, an
[all...]
/seL4-l4v-master/isabelle/src/Doc/Logics_ZF/document/
H A DZF.tex80 \cdx{restrict}& $[i, i] \To i$ & restriction of a function\\
91 \index{*"` symbol}\index{function applications}
164 In ZF, a function is a set of pairs. A ZF function~$f$ is simply an
166 $i\To i$. The infix operator~{\tt`} denotes the application of a function set
199 \rm function space \\
281 single-valued binary predicate is also called a {\bf class function}.
286 function~$\lambda x. b[x]$. The resulting set consists of all $b[x]$
288 since it applies a function to every element of a set. The syntax is
329 this to be a set, the function'
[all...]
/seL4-l4v-master/l4v/isabelle/src/Doc/Logics_ZF/document/
H A DZF.tex80 \cdx{restrict}& $[i, i] \To i$ & restriction of a function\\
91 \index{*"` symbol}\index{function applications}
164 In ZF, a function is a set of pairs. A ZF function~$f$ is simply an
166 $i\To i$. The infix operator~{\tt`} denotes the application of a function set
199 \rm function space \\
281 single-valued binary predicate is also called a {\bf class function}.
286 function~$\lambda x. b[x]$. The resulting set consists of all $b[x]$
288 since it applies a function to every element of a set. The syntax is
329 this to be a set, the function'
[all...]
/seL4-l4v-master/HOL4/examples/dev/booth/
H A DboothDevScript.sml11 The main function takes the input (a,rm,rs,rn)
201 The initialisation function takes the input
239 APPLY_NEXTd applies the next state function t times
251 state function t times
310 MULTd is the main function.
/seL4-l4v-master/HOL4/src/num/theories/
H A Dprim_recScript.sml26 * The rule is an ML function:
308 * We start by defining a (higher order) function SIMP_REC and
315 * We then define a function PRIM_REC in terms of SIMP_REC and prove that:
430 * We proceed by defining a function PRIM_REC and proving that:
627 * arising from a measure function is wellfounded, which is really great!
/seL4-l4v-master/HOL4/src/quotient/examples/
H A Dtactics.sml163 fun TACTIC_ERR{function,message} =
165 origin_function = function,
168 fun failwith function =
169 raise TACTIC_ERR{function = function,message = ""};
/seL4-l4v-master/HOL4/src/coretypes/
H A DsumScript.sml21 (* the unique function asserted to exist by the axiom. *)
83 (* Define a representation function, REP_sum, from the type ('a,'b)sum to *)
85 (* function ABS_sum, and prove some trivial lemmas about them. *)
103 (* Define the injection function INL:'a->('a,'b)sum *)
107 (* Define the injection function INR:'b->( 'a,'b )sum *)
/seL4-l4v-master/HOL4/examples/algebra/group/
H A DgroupProductScript.sml64 Group Iterated Product over a function:
277 (* Group Iterated Product over a function. *)
325 Now the hard part: show (\e acc. op (f e) acc) is an accumulative function for ITSET.
489 (* Define a group function *)
494 (* overload on group function *)

Completed in 242 milliseconds

<<11121314151617181920>>