Searched refs:function (Results 176 - 200 of 876) sorted by relevance
1234567891011>>
/seL4-l4v-master/HOL4/src/num/arith/src/ |
H A D | Sub_and_cond.sml | 26 fun failwith function = 28 origin_function = function, 198 (* enclose the subtraction operator. This function is not as delicate as it *) 211 (* Also eliminates the predecessor function, PRE. *)
|
H A D | Gen_arith.sml | 20 fun failwith function = raise (mk_HOL_ERR "Gen_arith" function ""); 32 (* The internal function uses failure to denote that the expression *) 76 (* The function detects multiplications in which both of the arguments are *)
|
/seL4-l4v-master/HOL4/src/opentheory/postbool/ |
H A D | Logging.sig | 35 [set_tyop_name_handler h] installs h as the function used to create an OpenTheory name from a HOL4 type operator name when the OpenTheoryMap does not already have a mapping for the HOL4 name.
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | Pretype.sig | 59 [mk_fun_ty (dom,rng)] Makes the pretype corresponding to the function space
|
/seL4-l4v-master/HOL4/src/pfl/examples/ |
H A D | zero.sml | 2 (* Constant zero function. *) 28 (* Indexed function definition *) 41 (* Domain of the function. *) 269 (* Theorem showing that exec BIG = zero in the domain of the function. *)
|
/seL4-l4v-master/HOL4/src/quotient/src/ |
H A D | quotient.sml | 19 (* This file defines the function "define_quotient_types", which takes *) 201 {abs} is a string, denoting the name of the new onto function from the 203 {rep} is a string, denoting the name of the new 1-1 function from the 278 Let each such set be represented by its characteristic function, 283 If P c, then c is a suitable function to represent an nty. 381 are one-to-one and onto. The ABS function is one-to-one on its 413 (* define function to yield representative objects of the new objects *) 426 (* define function to yield new objects from the base objects *) 710 message = "The following does not have the form of a simplification theorem for either\nrelation extension simplification or map function extension simplification:\n" ^ 756 Let each such set be represented by its characteristic function, [all...] |
/seL4-l4v-master/HOL4/src/ring/src/ |
H A D | ringLib.sig | 31 * - Reify is a function to transform a list of ring terms into
|
/seL4-l4v-master/HOL4/src/simp/src/ |
H A D | Cond_rewr.sig | 21 ascending order, according to a term_lt function which places
|
/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | Systeml.sig | 42 when fed to the compiler. For MoscowML, this is the identity function
|
/seL4-l4v-master/HOL4/tools/Holmake/mosml/ |
H A D | HM_Cline.sml | 38 (* this fupdcore function is used internally to build command-line options *)
|
/seL4-l4v-master/HOL4/tools/mlyacc/src/ |
H A D | link.sml | 47 (* returns function which takes a file name, invokes the parser on the file,
|
/seL4-l4v-master/HOL4/examples/CCS/ |
H A D | CCSSyntax.sml | 115 (* Given a list of terms, the function build_sum builds a CCS term which is 130 the function sum_to_fun sumL ARBtm n returns a function which associates 200 (* Conversion for evaluating a relabelling function fc (in conditional form). *)
|
H A D | ObsCongrConv.sml | 26 (* Define the function OC_SUB_CONV. *) 63 (* Define the function OC_DEPTH_CONV. *) 67 (* Define the function OC_TOP_DEPTH_CONV. *) 74 (* Define the function OC_SUBST for substitution in OBS_CONGR terms. *)
|
H A D | WeakLawsConv.sml | 99 (* Define the function OE_SUB_CONV. *) 150 (* Define the function OE_DEPTH_CONV. *) 154 (* Define the function OE_TOP_DEPTH_CONV. *) 161 (* Define the function OE_SUBST for substitution in WEAK_EQUIV terms. *)
|
/seL4-l4v-master/HOL4/examples/PSL/1.01/parser.mosmlyacc/ |
H A D | Lexer.lex | 25 (* Scan keywords as identifiers and use this function to distinguish them. *)
|
/seL4-l4v-master/HOL4/polyml/mlsource/ |
H A D | BuildExport.sml | 27 (* This function is the root of the "pre-built" compilers. It compiles in
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | LiteralNet.sml | 58 (* These function return OVER-APPROXIMATIONS! *)
|
H A D | PortableMlton.sml | 49 (* Timing function applications. *)
|
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/extract/ |
H A D | lisp_synthesisLib.sml | 34 (* the main synthesis function: shallow -> deep *)
|
/seL4-l4v-master/HOL4/examples/muddy/ |
H A D | fdd.sig | 38 relates to C types and function declarations in fdd.h:
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | LiteralNet.sml | 58 (* These function return OVER-APPROXIMATIONS! *)
|
H A D | PortableMlton.sml | 49 (* Timing function applications. *)
|
/seL4-l4v-master/HOL4/src/AI/proof_search/ |
H A D | psMCTS.sig | 29 (* search function *)
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | BackendIntermediateCodeSig.sml | 41 | BICEval of (* Evaluate a function with an argument list. *) 43 function: backendIC, 68 | BICBeginLoop of (* Start of tail-recursive inline function. *) 71 | BICLoop of (backendIC * argumentType) list (* Jump back to start of tail-recursive function. *)
|
/seL4-l4v-master/HOL4/src/Boolify/src/ |
H A D | Encode.sml | 68 (* Term encoding, as a function of types. The function gamma maps type *) 70 (* means failure. The function theta maps a type variable (say 'a) to a term *) 257 | NONE => (HOL_MESG("Couldn't define encode function for type "
|
Completed in 148 milliseconds
1234567891011>>