Searched refs:function (Results 126 - 150 of 876) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/polyml/basis/
H A DBasicStreamIO.sml54 Io { name = name, function = caller, cause = nonIo }
95 OutStreamClosed means that the writer's "close" function has been called.
149 raise Io { name = name, function = "input", cause = BlockingNotSupported }
292 raise Io { name = "", function = "getReader", cause = ClosedStream }
321 raise Io { name = "", function = "filePosIn", cause = ClosedStream }
359 raise Io { name = "", function = "filePosIn",
370 raise Io { name = "", function = "filePosIn",
373 raise Io { name = "", function = "filePosIn", cause = ClosedStream }
376 raise Io { name = "", function = "filePosIn",
389 raise Io { name = "", function
[all...]
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/
H A DTYPEIDCODE.sml58 polymorphic function is wrapped in a function that passes the type
174 print function will be used in polymorphic functions so must print "?". *)
176 val codeFn = mkProc(codePrettyString "fn", 1, "print-function", [], 0)
183 val printFn = (* Create a function to load the printer ref and apply to the args. *)
306 | FunctionType _ => SOME(fn _ => functionCode, ~1) (* Every function has the same code. *)
368 (* Apply the function we obtained to any type arguments. *)
420 (* Apply the function we obtained to any type arguments. *)
509 [] => (* Create a function that, when called, will extract the function fro
[all...]
/seL4-l4v-master/HOL4/examples/acl2/ml/
H A DpolytypicLib.sml18 (* Debug : Input to a lower function was of the wrong form *)
36 (* Create the different levels of exception given a function and message *)
66 (* Prints a function trace *)
158 (* function : *)
159 (* Represents a polytypic function, also holds its induction principle *)
170 type function = {const : term, definition : thm, induction : (thm * (term * (term * hol_type)) list) option} type
172 type functions = (hol_type,(string,function) dict ref) dict;
186 (* Level 3 : Output most intermediate results and function calls *)
259 (* Builds the graph of elements reachable from ''a under the function *)
371 (* Pushes all function application
2465 let val function = if exists_coding_function_precise target t name value
2494 let val function = if exists_source_function_precise t name value
3082 "The term given does not match the induction theorem and function") value
3146 val function = expanded_function_def conv create_conv get_def t value
[all...]
/seL4-l4v-master/HOL4/src/quotient/examples/
H A Dfinite_setScript.sml158 (* Fold1 computes the fold of a function on a list *)
161 (* For each such function its respectfulness theorem is proven. *)
165 (* The membership function to test if an element is a member of a list *)
220 (* Definition of Card function to measure the size of a finite set. *)
301 (* Definition of function to delete an element from a finite set; *)
443 (* Definition of Fold1 function to fold a function over a finite set. *)
456 (* Respectfulness theorem for the Fold1 function. *)
471 (* Definition of list2set function to convert a list to a set. *)
474 (* Respectfulness theorem for the list2set function
[all...]
H A DmsgScript.sml169 (* Definition of function to return all nonces from an expression. *)
178 (* Respectfulness theorem for the freenonces1 function. *)
199 (* Respectfulness theorem for the freeleft1 function. *)
221 (* Respectfulness theorem for the freeright1 function. *)
244 (* Respectfulness theorem for the is_nonce1 function. *)
/seL4-l4v-master/HOL4/polyml/libpolyml/
H A Dx86assembly_masm64.S23 ; rax: First argument to function. Result of function call.
24 ; rbx: Second argument to function.
31 ; r8: Third argument to function
32 ; r9: Fourth argument to function
33 ; r10: Fifth argument to function
52 UnusedRequestCode DB ? ; Byte: Io function to call.
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/
H A DCODEGEN_PARSETREE.sml111 (* Try this pipeline function *)
230 (* If it is referred to by a referenced function it is referenced. *)
273 function entry and exit. *)
277 (* Create an entry in the static environment for the function. *)
341 function calls. *)
345 This is used to decide whether to use a function for certain
370 let (* Put in a call to the expression as a function. *)
428 val functionLevel = newLevel level (* For the function. *)
494 function not afterwards. *)
520 | codeGenerate(Applic {f = Ident {value = ref function, expTyp
[all...]
/seL4-l4v-master/HOL4/src/IndDef/Manual/
H A Dpaper.tex63 {\small HOL} logic. But certain recursive type definitions and function
205 relation on $\alpha$. (Here, a relation is represented by a curried function;
228 function
304 function that takes as an argument a list of rules and automatically proves the
313 The {\small ML} function that implements this principle of inductive definition
329 \noindent The first argument to this function is a boolean flag which indicates
333 needed because this {\small ML} function can be used to define classes of
360 function \verb!new_inductive_definition! automatically proves the existence of
371 The following example {\small HOL} session shows how the function
402 function wit
[all...]
/seL4-l4v-master/HOL4/src/quotient/examples/lambda/
H A Dbarendregt.sml73 fun TACTIC_ERR{function,message} =
75 origin_function = function,
78 fun failwith function =
80 print_string ("Failure in Cond_rewrite: "^function^"\n")
82 raise TACTIC_ERR{function = function,message = ""});
98 (* SEARCH_matches applies the function f to every subterm of the
/seL4-l4v-master/HOL4/src/quotient/examples/sigma/
H A Dbarendregt.sml74 fun TACTIC_ERR{function,message} =
76 origin_function = function,
79 fun failwith function =
81 print_string ("Failure in Cond_rewrite: "^function^"\n")
83 raise TACTIC_ERR{function = function,message = ""});
99 (* SEARCH_matches applies the function f to every subterm of the
/seL4-l4v-master/isabelle/src/Doc/Logics/document/
H A DSequents.tex51 sequence. Thus, a theory designer can specify a function that takes
69 A sequence can be represented as a function --- a constructor for
70 further sequences --- by defining a binary {\em abstract} function
83 \verb|B| itself to refer to the function, and therefore the sequence
96 function called {\tt Trueprop}. So, an object
98 {\tt Trueprop(P)}\@. The name of the function is often hidden, so the
105 calculi, rather than use just one function that maps object-level
/seL4-l4v-master/l4v/isabelle/src/Doc/Logics/document/
H A DSequents.tex51 sequence. Thus, a theory designer can specify a function that takes
69 A sequence can be represented as a function --- a constructor for
70 further sequences --- by defining a binary {\em abstract} function
83 \verb|B| itself to refer to the function, and therefore the sequence
96 function called {\tt Trueprop}. So, an object
98 {\tt Trueprop(P)}\@. The name of the function is often hidden, so the
105 calculi, rather than use just one function that maps object-level
/seL4-l4v-master/HOL4/Manual/Translations/IT/Tutorial/
H A Dtool.tex96 \noindent The library \ml{taut} defines \ml{TAUT\_RULE}\footnote{The function \ml{TAUT\_RULE} has been replaced by a function called \ml{TAUT\_PROVE}
126 \ML{} function that maps a term $t_1$ to an equation:
137 Conversions are applied using the function:
144 and generates a conversion (\ie\ \ML{} function of type {\small\verb%term->thm%})
285 longer applicable to any subterms. The function \ml{TOP\_DEPTH\_CONV}
304 form. The conclusion of a theorem can be extracted with the \ML{} function
341 the infixed function:
441 system timer using the function:
505 \HOL{} already has a predefined function
[all...]
/seL4-l4v-master/HOL4/Manual/Tutorial/
H A Dtool.tex96 \noindent The library \ml{taut} defines \ml{TAUT\_RULE}\footnote{The function \ml{TAUT\_RULE} has been replaced by a function called \ml{TAUT\_PROVE}
126 \ML{} function that maps a term $t_1$ to an equation:
137 Conversions are applied using the function:
144 and generates a conversion (\ie\ \ML{} function of type {\small\verb%term->thm%})
285 longer applicable to any subterms. The function \ml{TOP\_DEPTH\_CONV}
304 form. The conclusion of a theorem can be extracted with the \ML{} function
341 the infixed function:
441 system timer using the function:
505 \HOL{} already has a predefined function
[all...]
/seL4-l4v-master/HOL4/src/num/arith/src/
H A DSolve_ineqs.sml30 fun failwith function = raise HOL_ERR{origin_structure = "Solve_ineqs",
31 origin_function = function,
136 (* combined inequality, and the second component is a function. When applied *)
137 (* to ():unit this function returns a theorem which states that under the *)
215 (* Given a list of inequalities (as bindings), this function determines *)
257 (* Given a list of inequalities represented by bindings, this function *)
262 (* inequalities that are assumptions of the theorem. The function fails if *)
265 (* The function assumes that none of the inequalities given are false, that *)
267 (* true are filtered out. The function then determines which variable to *)
H A DTerm_coeffs.sml27 fun failwith function = raise (mk_HOL_ERR "Term_coeffs" function "");
102 (* Given the coefficients representing two inequalities, this function *)
149 (* function also assumes that when a variable has a coefficient of one, it *)
180 (* function also assumes that when a variable has a coefficient of one, it *)
/seL4-l4v-master/HOL4/examples/dev/sw/
H A DcpsScript.sml33 (* CPS definitions. The invocation "CPS f" wraps a function in a CPS, in *)
58 (* Passing the identity function to a CPS function is the inverse of *)
59 (* CPSing the function *)
70 (* Wrapping a function in a CPS interface that takes 2 continuations. *)
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/
H A DcpsScript.sml33 (* CPS definitions. The invocation "CPS f" wraps a function in a CPS, in *)
58 (* Passing the identity function to a CPS function is the inverse of *)
59 (* CPSing the function *)
70 (* Wrapping a function in a CPS interface that takes 2 continuations. *)
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/
H A DcpsScript.sml33 (* CPS definitions. The invocation "CPS f" wraps a function in a CPS, in *)
58 (* Passing the identity function to a CPS function is the inverse of *)
59 (* CPSing the function *)
70 (* Wrapping a function in a CPS interface that takes 2 continuations. *)
/seL4-l4v-master/HOL4/examples/hardware/hol88/
H A DITL.ml8 % Test if an interval function only depends on the start time
15 % Make an interval function out of a signal %
21 % Test if an interval function is a constant function %
27 % Make an interval function out of a constant %
/seL4-l4v-master/HOL4/src/coretypes/
H A DposetScript.sml54 ``function a b (f : 'a -> 'b) = !x. a x ==> b (f x)``);
186 (function t s, \f g. !x. t x ==> r (f x) (g x))``);
322 poset p /\ complete p /\ function (carrier p) (carrier p) f /\
366 poset p /\ complete p /\ function (carrier p) (carrier p) f /\
410 poset p /\ complete p /\ function (carrier p) (carrier p) f /\
/seL4-l4v-master/HOL4/src/portableML/
H A DOldPP.sig55 are placed in the stream by various function calls listed below.
69 of a string consumer, a specified linewidth, and a flush function
90 [dest_ppstream ppstrm] extracts the linewidth, flush function, and
110 (calculating its width using the UTF8.size function).
126 consumer associated with ppstrm); executes the flush function
/seL4-l4v-master/isabelle/src/Doc/Tutorial/document/
H A Dsets.tex10 function is a set, and the inverse image of a function maps sets to sets.
446 \indexbold{updating a function}%
456 \isa{(f(x:=y))\ z} we are applying an updated function to an
467 The \bfindex{identity function} and function
489 A function may be \textbf{injective}, \textbf{surjective} or \textbf{bijective}:
502 of \isa{inj_on} lets us express that a function is injective over a
504 functions are total; in some cases, a function's natural domain is a subset
509 \textbf{inverse}\indexbold{inverse!of a function}
[all...]
/seL4-l4v-master/l4v/isabelle/src/Doc/Tutorial/document/
H A Dsets.tex10 function is a set, and the inverse image of a function maps sets to sets.
446 \indexbold{updating a function}%
456 \isa{(f(x:=y))\ z} we are applying an updated function to an
467 The \bfindex{identity function} and function
489 A function may be \textbf{injective}, \textbf{surjective} or \textbf{bijective}:
502 of \isa{inj_on} lets us express that a function is injective over a
504 functions are total; in some cases, a function's natural domain is a subset
509 \textbf{inverse}\indexbold{inverse!of a function}
[all...]
/seL4-l4v-master/HOL4/src/string/Manual/
H A Ddescription.tex17 describing concrete types used by the function \ml{define\_type}, the type
27 function \ml{ASCII} to the eight boolean values of its standard ascii character
36 in logic by a value of type \ml{ascii} constructed using the function constant
40 library using the function \ml{define\_type} from the \HOL\ recursive types
57 \index{function definitions!on type {\tt ascii}|(}
62 loaded into \HOL, one can use this rule of definition to define a function that
74 \noindent In fact, any function whatsoever on the \ml{ascii} is definable
77 \index{function definitions!on type {\tt ascii}|)}
88 the function \ml{ASCII} is injective:
124 using the function \m
[all...]

Completed in 154 milliseconds

1234567891011>>