Searched refs:function (Results 151 - 175 of 876) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/
H A DTYPECHECK_PARSETREE.sml132 (* 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 DPolyVectorOperations.sml47 (* 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 DSignal.sml99 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 DForeign.581.sml79 (* 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 DinlineCompile.sml9 (* 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 Dexor32.ml49 (* 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 Dclosure.sml11 (* Close the function variable by variable *)
54 (* Close the function variable by variable *)
/seL4-l4v-master/HOL4/src/num/arith/src/
H A DNorm_bool.sml25 fun failwith function = raise (mk_HOL_ERR "Norm_bool" function "");
/seL4-l4v-master/HOL4/src/quotient/Manual/
H A Dquotient.tex211 %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 Dtactics.sig58 val TACTIC_ERR{function,message} =
60 origin_function = function,
/seL4-l4v-master/HOL4/src/ring/src/
H A Dquote.sml12 fun QUOTE_ERR function message =
14 origin_function = function,
/seL4-l4v-master/HOL4/src/simp/src/
H A DOpening.sig7 * The first argument should be a function implementing reflexivity
13 * Providing these two returns a function which implements a
H A DTravrules.sig47 * function will return a theorem showing REL(t1,t2) for the
60 * the function CONGRULE.
/seL4-l4v-master/HOL4/tools/Holmake/
H A Dinternal_functions.sig65 [function_call(fnname, args, eval)] evaluates the internal function
69 by the eval function.
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/
H A DTYPEIDCODESIG.sml40 (* 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 Ddebugger.scala19 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 Ddebugger.scala19 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 Dx86assembly_masm32.S23 ; 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 DfunctionEncodeLib.sml16 (* 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 Ddescription.tex37 \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 DCODETREE_SIMPLIFIER.sml166 | 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 Dmod.ml4 % DESCRIPTION : Defines MOD function for natural numbers and proves %
/seL4-l4v-master/HOL4/polyml/samplecode/ide/
H A Duse.sml2 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 DLibrary.sml38 (* 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 DIntDP_Munge.sig43 generalisations introduced). The function f will take a theorem of the

Completed in 318 milliseconds

1234567891011>>