/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | BasicStreamIO.sml | 54 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 D | TYPEIDCODE.sml | 58 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 D | polytypicLib.sml | 18 (* 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 D | finite_setScript.sml | 158 (* 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 D | msgScript.sml | 169 (* 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 D | x86assembly_masm64.S | 23 ; 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 D | CODEGEN_PARSETREE.sml | 111 (* 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 D | paper.tex | 63 {\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 D | barendregt.sml | 73 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 D | barendregt.sml | 74 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 D | Sequents.tex | 51 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 D | Sequents.tex | 51 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 D | tool.tex | 96 \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 D | tool.tex | 96 \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 D | Solve_ineqs.sml | 30 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 D | Term_coeffs.sml | 27 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 D | cpsScript.sml | 33 (* 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 D | cpsScript.sml | 33 (* 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 D | cpsScript.sml | 33 (* 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 D | ITL.ml | 8 % 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 D | posetScript.sml | 54 ``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 D | OldPP.sig | 55 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 D | sets.tex | 10 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 D | sets.tex | 10 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 D | description.tex | 17 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...] |