/seL4-l4v-master/HOL4/examples/misc/ |
H A D | contMonadScript.sml | 8 don't need to hide the function under a constructor, but this does
|
/seL4-l4v-master/HOL4/examples/muddy/ |
H A D | bvec.sig | 55 relates to C types and function declarations in bvec.h:
|
/seL4-l4v-master/isabelle/src/HOL/Hahn_Banach/document/ |
H A D | root.tex | 47 supremum (w.r.t.\ the function order) and extension of non-maximal functions.
|
/seL4-l4v-master/isabelle/src/HOL/Statespace/document/ |
H A D | root.tex | 45 spaces. The state is represented as a function from (abstract) names
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Atom.sig | 50 (* A total comparison function for atoms. *)
|
H A D | PortableMosml.sml | 54 (* Timing function applications. *)
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Tutorial/document/ |
H A D | advanced0.tex | 32 %proof time. In HOL you may have to work hard to define a function, but proofs
|
H A D | fp.tex | 146 \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 D | root.tex | 47 supremum (w.r.t.\ the function order) and extension of non-maximal functions.
|
/seL4-l4v-master/l4v/isabelle/src/HOL/Statespace/document/ |
H A D | root.tex | 45 spaces. The state is represented as a function from (abstract) names
|
/seL4-l4v-master/HOL4/examples/bootstrap/ |
H A D | source_valuesScript.sml | 13 (* Since strings are not in the representation, we have a function that
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
H A D | BASE_PARSE_TREE.sml | 217 (* 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 D | ThreadLib.sml | 25 (* This applies a function while a mutex is being held.
|
H A D | VectorOperations.sml | 51 (* 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 D | Thread.sml | 35 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 D | syntax.tex | 39 & | & \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 D | syntax.tex | 39 & | & \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 D | fp.tex | 146 \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 D | ZF.tex | 80 \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 D | ZF.tex | 80 \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 D | boothDevScript.sml | 11 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 D | prim_recScript.sml | 26 * 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 D | tactics.sml | 163 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 D | sumScript.sml | 21 (* 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 D | groupProductScript.sml | 64 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 *)
|