/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
H A D | TYPECHECK_PARSETREE.sml | 132 (* Returns a function which can be passed to unify or apply to 264 let (* Make arg->'a, and unify with the function. *) 284 Handlers: the handling patterns are unified against a function from exn -> the result type of the 375 This is used for lists, function values (fn .. => ...), 457 (* Get the current overload set for the function and return a new 464 (* Look up the current overloading for this function. *) 569 (* Apply the function to the argument and return the result. *) 759 (* Apply the function to the argument and return the result. *) 766 polymorphic and wrap a function round it. *) 771 (* Test to see if we have a function [all...] |
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | PolyVectorOperations.sml | 47 (* Apply a function to each element in turn *) 68 (* Fold a function over a array. *) 111 (* Apply a function to each element in turn and update the array with the
|
H A D | Signal.sml | 99 The `Signal.signal` function takes as its arguments a signal number and an 102 ignored (blocked) or `SIG_HANDLE`, which allows a handler function to be installed. 112 A handler function installed using `SIG_HANDLE` is run as a separate thread
|
H A D | Foreign.581.sml | 79 (* Initialise to zero. That means the function won't be 84 We need to execute the function and set it. *)
|
/seL4-l4v-master/HOL4/examples/dev/ |
H A D | inlineCompile.sml | 9 (* replace the function calls with their bodies in the function main (inline *) 13 (* instead of being restricted to the scope of a single function body. *) 15 (* In order to implement the rewriting of the main function, *) 56 (* where the def is the function defined in terms of Seq, Par, Ite, Rec *) 140 raise ERR "CompileExp2" "attempt to compile non-function")
|
/seL4-l4v-master/HOL4/examples/dev/Fact32/ |
H A D | exor32.ml | 49 (* Define a Verilog module as an ML string (XOR32vDef), a function to *) 52 (* instances) and a function to print a HOL term ``XOR32(in1,in2,out)`` as *)
|
/seL4-l4v-master/HOL4/examples/dev/sw2/ |
H A D | closure.sml | 11 (* Close the function variable by variable *) 54 (* Close the function variable by variable *)
|
/seL4-l4v-master/HOL4/src/num/arith/src/ |
H A D | Norm_bool.sml | 25 fun failwith function = raise (mk_HOL_ERR "Norm_bool" function "");
|
/seL4-l4v-master/HOL4/src/quotient/Manual/ |
H A D | quotient.tex | 211 %in particular lists, pairs, sums, options, and function types. 344 of function types. 357 for a function type, 360 for the function's domain and range, are the heart of this paper, 399 their extension for aggregate and function types, 402 for lifting aggregate and function types. 404 %The quotient extension theorem for function types 524 represented in HOL as a curried function 796 The reason is that not all functions which are elements of the function 802 the set of functions from $\tau$ to $\tau$ may contain a function [all...] |
/seL4-l4v-master/HOL4/src/quotient/examples/ |
H A D | tactics.sig | 58 val TACTIC_ERR{function,message} = 60 origin_function = function,
|
/seL4-l4v-master/HOL4/src/ring/src/ |
H A D | quote.sml | 12 fun QUOTE_ERR function message = 14 origin_function = function,
|
/seL4-l4v-master/HOL4/src/simp/src/ |
H A D | Opening.sig | 7 * The first argument should be a function implementing reflexivity 13 * Providing these two returns a function which implements a
|
H A D | Travrules.sig | 47 * function will return a theorem showing REL(t1,t2) for the 60 * the function CONGRULE.
|
/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | internal_functions.sig | 65 [function_call(fnname, args, eval)] evaluates the internal function 69 by the eval function.
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ |
H A D | TYPEIDCODESIG.sml | 40 (* Generate a function of the form t*int->pretty for values of type t. *) 42 (* Generate a function of the form (t,t) -> bool. *)
|
/seL4-l4v-master/isabelle/src/Pure/Tools/ |
H A D | debugger.scala | 19 sealed case class Debug_State(pos: Position.T, function: String) 46 case Some(d) => d.function 120 case (pos, function) => Debug_State(pos, function)
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Tools/ |
H A D | debugger.scala | 19 sealed case class Debug_State(pos: Position.T, function: String) 46 case Some(d) => d.function 120 case (pos, function) => Debug_State(pos, function)
|
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | x86assembly_masm32.S | 23 ; eax: First argument to function. Result of function call. 24 ; ebx: Second argument to function. 46 UnusedRequestCode DB ? ; Byte: Io function to call.
|
/seL4-l4v-master/HOL4/examples/acl2/ml/ |
H A D | functionEncodeLib.sml | 16 (* derivation of function type for encode/decode et al... *) 24 (* not collected. A function should be created to log this and use it *) 26 (* 2) (Minor) When a coding function is added its form is not checked *) 146 print "The term is not an instance of function application." 1312 (* a) If the term is matched by function in !terminals then REFL term *) 1314 (* b) If the term is matched by a polytypic theorem, ie. a function *) 1333 (* The add_extended_terminal function can also determine the list of *) 1531 (* Returns a function that finds the outermost leftmost constructed term *) 1534 (* returns that function that returns the last argument from terms *) 1536 (* Fails if the theorems supplied are not function clause 1644 "Theorems and function term supplied use different function constants") value 1807 val function = list_mk_comb(left,map (fn (a,b) => (mk_var(implode (base26 a),b))) value 4191 let val (function,missing) = clause_to_case thm value [all...] |
/seL4-l4v-master/HOL4/src/pred_set/Manual/ |
H A D | description.tex | 37 \noindent The infix function constant \ml{IN} defined here constitutes the 40 one function. 94 \noindent The function \ml{GSPEC} takes a function \ml{f :\ 'b -> ('a \# bool)} 115 above, let \ml{f} in this definition be the function 134 {\small\verb!"{!$E$\verb! | !$P$\verb!}"!}. The built-in \ML\ function 139 The call made to this function extends the \HOL\ parser so that a quotation of 317 function of the values of \ml{n} and \ml{m}, and so by eliminating the 328 {\small\verb!"{!$E$\verb! | !$P$\verb!}"!} will not be an injective function of 552 built-in \ML\ function \m [all...] |
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | CODETREE_SIMPLIFIER.sml | 166 | simpGeneral context (Eval {function, argList, resultType}) = 167 SOME(specialToGeneral(simpFunctionCall(function, argList, resultType, context, RevList[]))) 464 an inline function respectively if that's possible. Getting that also involves 483 | simpSpecial (Eval {function, argList, resultType}, context, tailDecs) = 484 simpFunctionCall(function, argList, resultType, context, tailDecs) 556 functions. The main function body takes its arguments on 557 the stack (or in registers) and the auxiliary inline function, 559 calls it. If the main function is recursive it will first 560 call the inline function which is why the pair are mutually 562 As far as possible we want to use the main function sinc [all...] |
/seL4-l4v-master/HOL4/examples/hardware/hol88/mos-count/ |
H A D | mod.ml | 4 % DESCRIPTION : Defines MOD function for natural numbers and proves %
|
/seL4-l4v-master/HOL4/polyml/samplecode/ide/ |
H A D | use.sml | 2 Title: Modified version of the "use" function which saves state 22 This is an example version of the "use" function that the IDE may call 24 function that saves the state and dependencies in ".save" and ".deps" files 39 when this function is called and convert them to absolute paths using the
|
/seL4-l4v-master/HOL4/src/HolSmt/ |
H A D | Library.sml | 38 (* returns a function that returns the next character in 'instream' 63 (* Takes a function that returns characters 64 (cf. 'get_buffered_char'), returns a function that returns 211 (* auxiliary function: fails unless 's' is a subterm of 't' with
|
/seL4-l4v-master/HOL4/src/integer/ |
H A D | IntDP_Munge.sig | 43 generalisations introduced). The function f will take a theorem of the
|