Searched refs:function (Results 276 - 300 of 876) sorted by relevance

<<11121314151617181920>>

/seL4-l4v-master/HOL4/src/datatype/mutrec/
H A DConsThms.sml42 (* This function divides up a list of applied constructors into a list
64 (* This function proves that constructors are distinct, ie, for each TY
121 (* the following function takes the constructor first in the list, (say
139 (* this function makes all the conjuncts for one type *)
222 We apply the appropriate distinctness function, getting
262 (* This function proves that constructors are one-to-one, ie, for each TY
353 extraction function will be called CON_arg.) *)
442 a pair consisting of the definition of the function and the name of
443 the function defined. *)
524 (* This function prove
[all...]
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/
H A DDEBUGGER_.sml66 (* Global function entries. These could be in storage allocated by the RTS. *)
67 (* Specialised option type here. Because a function is always boxed this
215 return a function because we will use applyToInstanceType to apply it to the
253 because the next reference could be inside an inner function.
405 (* Add debugging calls on entry and exit to a function. *)
436 (* At the start of the function:
440 4. Call the global onEntry function if it's set
441 5. Call the local onEntry function if it's set *)
454 to be passed to the body of the function so that it is included in the
486 (* Restore the state. Used both if the function return
[all...]
/seL4-l4v-master/HOL4/examples/dev/
H A Dvsynth.sml46 (* Error reporting function *)
156 print "\nis not a function type\n";
157 raise ERR "dest_unop_type" "not a function type")
172 print "\nis not a function type\n";
173 raise ERR "dest_binop_type" "not a function type")
468 (* ClockvInst out n "clk" prints, using function out, an instance of Clock *)
517 handle e => (print "ML function associated in vsynth_lib with:\n";
/seL4-l4v-master/HOL4/examples/elliptic/c_output/
H A Dc_outputLib.sml200 ) ("Unknown function '"^f_name^"'!")
242 ("Unknown boolean function '"^(term_to_string exp)^"'!");
251 (syntax_error true ("Unknown boolean function '"^(term_to_string exp)^"'!"); (false, ""));
436 ("The function '"^fun_name^"' is not a function on 32-bit words!");
612 (print "The main function is not in the list of definitions!\n";fail()) else ();
619 val _ = print "The following constants are unkown to the C-export function. Please add additional definitions or rewrites:\n";
/seL4-l4v-master/HOL4/src/integer/
H A DOmegaSymbolic.sml106 This function attempts to prove |- EVERY fst_nzero ^t
140 This function attempts to prove |- EVERY fst1 ^t
166 This function attempts to prove |- EVERY (\p. FST p <= ^m) ^t
198 defining the corresponding row function (conjuncts of
358 This function expands it into an equation of the form
408 Every ci is a valid Omega leaf. This function converts the body
569 fully normalised leaves. This function picks one of the quantifiers
/seL4-l4v-master/HOL4/src/portableML/
H A DPortable.sml527 * A hash function used for various tasks in the system. It works fairly *
529 * argument should be a prime. The function then takes a string and *
682 * Invoking a function with a flag temporarily assigned to the given value. *
741 A function that strips leading (nested) comments and whitespace
780 * pfun = item printing function
781 * dfun = delimiter printing function
782 * bfun = break printer function
/seL4-l4v-master/HOL4/polyml/basis/
H A DLibraryIOSupport.sml18 (* This function provides wrappers for the RTS file descriptors to construct
173 (* If evaluating the function raises EAGAIN or EWOULDBLOCK we return NONE
277 (* Unlike the other functions "avail" is a function returning
278 an option, not an optional function. *)
389 (* Unlike the other functions "avail" is a function returning
390 an option, not an optional function. *)
462 This applies a function while a mutex is being held. *)
H A DBoolArray.sml56 The equality function we're using tests all the bytes so we need to initialise them. *)
126 (* Internal function which subscripts the vector assuming that
234 apply the function beyond the last bit. *)
261 apply the function beyond the last bit. *)
363 (* Internal function for updating a bit assuming the bounds
399 (* Exported update function. *)
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/
H A DmechReasoning.sml290 (* the characteristic function *)
293 val f_c = mk_pabs (initV, subst rules (calculate_outs post_st outs)); (* the charateristic function *)
299 (* the stack function *)
317 (* Given an basic block, the charateristic function on inputs and outputs are derived by symbolic simulation *)
415 (* the characteristic function of SC *)
515 (* Given a TR, the charateristic function on inputs and outputs are derived by the TR_RULE *)
550 val cj_cond = subst rules instance1 (* the condition function *)
555 fun mk_cond_f cond_t ins = (* the condition function *)
616 (* the characteristic function *)
686 (* the characteristic function *)
[all...]
/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/
H A Dconv.tex22 is an \ML\ function of type \ml{conv} (\ie\ a conversion) that
149 this exception appropriately. The standard function \ml{QCONV} is
319 subterm of a term, the function \ml{DEPTH\_CONV} can be applied to $c$:
363 \noindent The function \ml{TOP\_DEPTH\_CONV}
386 Finally, the simpler function \ml{ONCE\_DEPTH\_CONV} is provided:
507 The function \ml{FIRST\_CONV}
545 The function \ml{EVERY\_CONV} applies a list of conversions in sequence.
625 \noindent The function \ml{SUB\_CONV}
821 and the successor function \ml{SUC}, then:
916 done component-wise, and function application
[all...]
H A DHolBdd.tex110 In Version~1 there was a function, called
269 Initialisation is done with the ML function
309 The function
320 The function
333 using the function \t{stats}
393 The function \t{toBool} returns \t{true} on TRUE and \t{false} on FALSE.
421 dynamically. The function
430 The function
478 \Muddy{} provides a function for general purpose simultaneous
504 Variables can be renamed using the function \
[all...]
/seL4-l4v-master/HOL4/Manual/Translations/IT/Tutorial/binomial/
H A Dbinomial.tex136 $\obj{CHOOSE}\,n\,k$, where $\obj{CHOOSE}$ is a function defined by
192 says that any base case and inductive case identifies a unique function,
202 Given the theorem \verb@prim_rec@, the builtin function
203 \verb@prove_rec_fn_exists@ can prove that there is a function that satisfies
218 easy to prove there is a function which satisfies the original three
359 which can be coded as the \ML{} function \verb@SPEC_EQ@:
471 Hilbert's $\epsilon$-operator to specify a function \verb@Id@ such that
474 is unique. The first step is to prove that there exists a function \verb@Id@
554 a function \verb@Inv@ so that, if \verb@Group plus@ holds, then the
555 element \verb@Inv plus a@ is an inverse of \verb@a@. The function
[all...]
/seL4-l4v-master/HOL4/Manual/Tutorial/binomial/
H A Dbinomial.tex136 $\obj{CHOOSE}\,n\,k$, where $\obj{CHOOSE}$ is a function defined by
192 says that any base case and inductive case identifies a unique function,
202 Given the theorem \verb@prim_rec@, the builtin function
203 \verb@prove_rec_fn_exists@ can prove that there is a function that satisfies
218 easy to prove there is a function which satisfies the original three
359 which can be coded as the \ML{} function \verb@SPEC_EQ@:
471 Hilbert's $\epsilon$-operator to specify a function \verb@Id@ such that
474 is unique. The first step is to prove that there exists a function \verb@Id@
554 a function \verb@Inv@ so that, if \verb@Group plus@ holds, then the
555 element \verb@Inv plus a@ is an inverse of \verb@a@. The function
[all...]
/seL4-l4v-master/HOL4/src/meson/test/
H A Dselftest.sml1682 (!Xf. function(Xf) ==> subclass(Xf,cross_product(universal_class,universal_class))) /\
1683 (!Xf. function(Xf) ==> subclass(compose(Xf,inverse(Xf)),identity_relation)) /\
1684 (!Xf. subclass(Xf,cross_product(universal_class,universal_class)) /\ subclass(compose(Xf,inverse(Xf)),identity_relation) ==> function(Xf)) /\
1685 (!Xf X. function(Xf) /\ member(X,universal_class) ==> member(image(Xf,X),universal_class)) /\
1689 (function(choice)) /\
1691 (!Xf. one_to_one(Xf) ==> function(Xf)) /\
1692 (!Xf. one_to_one(Xf) ==> function(inverse(Xf))) /\
1693 (!Xf. function(inverse(Xf)) /\ function(Xf) ==> one_to_one(Xf)) /\
1698 (!Xf. operation(Xf) ==> function(X
[all...]
/seL4-l4v-master/HOL4/Manual/Description/
H A DHolBdd.tex110 In Version~1 there was a function, called
269 Initialisation is done with the ML function
309 The function
320 The function
333 using the function \t{stats}
393 The function \t{toBool} returns \t{true} on TRUE and \t{false} on FALSE.
421 dynamically. The function
430 The function
478 \Muddy{} provides a function for general purpose simultaneous
504 Variables can be renamed using the function \
[all...]
/seL4-l4v-master/HOL4/src/1/
H A Ddep_rewrite.sml118 (* These take as argument a thm_tactic, a function which takes a *)
183 fun TACTIC_ERR{function,message} =
185 origin_function = function,
188 fun failwith function =
190 print_string ("Failure in dep_rewrite: "^function^"\n")
192 raise TACTIC_ERR{function = function,message = "Failure in dep_rewrite"});
303 (* APPLY_IMP_THEN ttac th is a dependent rewriting function, *)
395 (* TAC_DEP turns a tactic into a dependent rewriting function. *)
405 (* DEP_TAC turns a dependent rewriting function int
[all...]
/seL4-l4v-master/HOL4/examples/dev/sw2/examples/
H A Darm_compiler_demoScript.sml23 arm_progLib can be used. The compiler's top-level function is
53 The compiler expects def to be a function where variables have names
62 memory locations (m0,m1,m2,etc), f over function names,
80 restrictions regarding varaible names in function calls.)
155 the definition of the function, i.e.
340 (* TEST: function in-lining *)
423 Use the option "PushProcedure ([],0)" when the function to be compiled contains
450 Example: the function c1 (below) uses registers 11 and 12 as temporaries and
451 function c2 (also below) depends on the fact that the values in registers 11
474 (* So far we have required that procedure/function call
[all...]
/seL4-l4v-master/isabelle/src/Doc/Logics/document/
H A DHOL.tex120 function types, is overloaded with arity {\tt(term,\thinspace
176 Where function types are involved, Isabelle's unification code does not
456 & range of a function \\[1ex]
570 avoid complications involving function types in unification. The isomorphisms
751 %definition, $f$ is the abstraction function and $A$ is the set of valid
864 \cdx{inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & inverse function
882 rules. Reasoning about function composition (the operator~\sdx{o}) and the
955 {Chap.\ts\ref{chap:simplification}}), there is a special infix function
1150 \cdx{Suc} & $nat \To nat$ & & successor function\\
1240 %define a higher-order function, w
[all...]
/seL4-l4v-master/l4v/isabelle/src/Doc/Logics/document/
H A DHOL.tex120 function types, is overloaded with arity {\tt(term,\thinspace
176 Where function types are involved, Isabelle's unification code does not
456 & range of a function \\[1ex]
570 avoid complications involving function types in unification. The isomorphisms
751 %definition, $f$ is the abstraction function and $A$ is the set of valid
864 \cdx{inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & inverse function
882 rules. Reasoning about function composition (the operator~\sdx{o}) and the
955 {Chap.\ts\ref{chap:simplification}}), there is a special infix function
1150 \cdx{Suc} & $nat \To nat$ & & successor function\\
1240 %define a higher-order function, w
[all...]
/seL4-l4v-master/HOL4/Manual/Quick/
H A Dquick.tex29 \hol{TotalDefn}{Define} \var{term} & function definition \\
219 \hol{Conv}{SKOLEM_CONV} & proves the existence of a Skolem function \\[4pt]
295 \hol{Lib}{time} \var{function} & measure how long a function application takes \\
298 \hol{Count}{apply} \var{function} & returns the theorem count for a function application \\
/seL4-l4v-master/HOL4/examples/Crypto/TWOFISH/
H A DtwofishScript.sml6 bijective F function made up of four key-dependent 8-by-8-bit S-boxes,
235 (* function works in k stages. In each stage, the four bytes are each *)
287 (* The words of the expanded key are defined using the h function. For Ai *)
399 (* The function FF is a key-dependent permutation on 64-bit values *)
411 (*-------------Forward round used by the encrypting function-----------------*)
436 (*-------------Backward round used by the decrypting function----------------*)
/seL4-l4v-master/HOL4/examples/lambda/basics/
H A DbinderLib.sml57 to prove that such a function actually exists. The RHS of any
59 attempt a recursion that is not be justified. This function
458 ("Couldn't prove function with swap over range - \n\
466 ("Couldn't prove function with swap over range - \n\
492 ("Couldn't prove function with swap over range - \n\
504 ("Couldn't prove function with swap over range - \n\
/seL4-l4v-master/HOL4/src/HolSmt/
H A DSmtLib.sml26 (* (HOL type, a function that maps the type to its SMT-LIB sort name) *)
58 (* (HOL term, a function that maps a pair (rator, rands) to an
319 (* SMT-LIB type and function names are uniformly generated as "tN"
359 arguments of base type, but not to arguments of function type;
364 offending function type to a fresh base type, and by abstracting
366 correct (abstracted) type. Note that the same function/operator
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/
H A DBackendIntermediateCode.sml184 | BICEval of (* Evaluate a function with an argument list. *)
186 function: backendIC,
212 | BICBeginLoop of (* Start of tail-recursive inline function. *)
215 | BICLoop of (backendIC * argumentType) list (* Jump back to start of tail-recursive function. *)
399 BICEval {function, argList, resultType} =>
409 [ pretty function, PrettyBreak(1, 0), prettyArgType resultType, PrettyBreak(1, 0), prettyArgs ]
/seL4-l4v-master/HOL4/src/HolQbf/
H A DQDimacs.sml80 (* auxiliary function to strip off quantifiers over Boolean variables *)
145 (* into a function that can be passed to 'read_qdimacs_file' as its *)
167 (* a function (i.e., the result only depends on its argument), and *)

Completed in 162 milliseconds

<<11121314151617181920>>