Searched refs:function (Results 76 - 100 of 876) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/src/integer/testing/
H A Dreadproblemfile.sig16 and applies the function f to each term and the value of the "previous"
23 [app f is] applies function f to the terms in stream is and ignores the
/seL4-l4v-master/HOL4/src/simp/src/
H A DCache.sig17 The RCACHE variant of this function should be used for those
21 parameter to RCACHE is a function that when applied to a term that
H A DSequence.sml15 (*Head and tail. Beware of calling the sequence function twice!!*)
53 the function prelem should print the element number and also the element*)
62 (*Map the function f over the sequence, making a new sequence*)
95 (*accumulating a function over a sequence; this is lazy*)
/seL4-l4v-master/HOL4/tools/Holmake/
H A DHolmake_types.sig48 command information (using the get_rule_info function). The warn
49 function is used to output warning messages about the rule_info. *)
/seL4-l4v-master/HOL4/polyml/basis/
H A DIO.sml24 exception Io of {name : string, function : string, cause : exn}
34 exception Io of {name : string, function : string, cause : exn}
/seL4-l4v-master/HOL4/src/metis/
H A Dselftest.sml23 fun normalForms_test (fname, function :conv, problem, result) = let
33 function (* 'b -> 'a *)
H A DfolMapping.sig20 {higher_order : bool, (* Application is a first-order function *)
/seL4-l4v-master/l4v/tools/c-parser/testfiles/
H A Dparse_complit.c57 int function(void) function
/seL4-l4v-master/HOL4/src/datatype/mutrec/
H A DMutRecDef.sml33 fun MUT_REC_ERR {function,message} = HOL_ERR{origin_structure = "MutRecDef",
34 origin_function = function,
46 | _ => raise MUT_REC_ERR {function = "dest_fun",
47 message = "Not a function type"})
53 | _ => raise MUT_REC_ERR {function = "dest_prod",
60 | _ => raise MUT_REC_ERR{function = "dest_sum",
116 else Raise (MUT_REC_ERR {function = "find_witnesses",
165 raise MUT_REC_ERR{function="type_num",
235 (* Our next goal is to define a function (called joint_name^"_select",
236 I'll refer to it as the joint select function) tha
[all...]
/seL4-l4v-master/HOL4/examples/dev/
H A DFactScript.sml65 (* Implement iterative function as a step to implementing factorial *)
87 (* Implement a function Fact to compute SND(FactIter (n,1)) *)
93 (* Verify Fact is indeed the factorial function *)
103 (* To implement ``$*`` we build a naive iterative multiplier function *)
199 (* Finally, create implementation of FACT (HOL's native factorial function) *)
/seL4-l4v-master/HOL4/src/num/arith/src/
H A DSol_ranges.sml32 fun failwith function = raise HOL_ERR{origin_structure = "Sol_ranges",
33 origin_function = function,
143 (* as bindings). The function fails if it can't find such values. *)
145 (* The function tries permutations of the variables, because the ordering *)
149 (* so, for a large number of variables, the function could execute for a *)
H A DExists_arith.sml32 fun failwith function = raise HOL_ERR{origin_structure = "Exists_arith",
33 origin_function = function,
75 (* This function proves an existentially quantified arithmetic formula given *)
H A DSolve.sml26 fun failwith function = raise (mk_HOL_ERR "Solve" function "")
116 (* The function fails if the application of `conv' to the negation of the *)
119 (* If use of this function succeeds then the input term will necessarily *)
/seL4-l4v-master/HOL4/src/1/
H A DPmatchHeuristics.sig63 choose the best results. For technical reasons, this function
67 Heu_fun initialises the functions and returns a compare function
68 and a function heu_fun' which provides heuristics. As long as
71 function is choosen. *)
87 explicit list of heuristics and a compare function *)
H A DMutual.sml26 (* Internal function: *)
63 (* Internal function: *)
87 (* Internal function: *)
113 (* Internal function: GTAC *)
132 (* Internal function: TACF *)
161 (* TACF is a strictly local function, used only to define TACS, below. *)
205 (* Internal function: TACS *)
219 (* TACS is a strictly local function, used only in MUTUAL_INDUCT_THEN. *)
232 (* Internal function: GOALS *)
239 (* GOALS is a strictly local function, use
[all...]
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/
H A DCODETREE_CODEGEN_CONSTANT_FUNCTIONS.sml19 If a function has an empty closure it can be code-generated immediately. That may allow
63 (* Code-generate a function or set of mutually recursive functions that contain no free variables
75 (* If we are code-generating a function immediately we make a one-word
77 After it is locked this becomes the closure of the function. By creating
79 we actually compile the function. *)
98 (* Create a "closure" for the function. *)
137 possible to code-generate the group if no function has a free-variable
138 outside the group. Each function must have at least one free
305 (* Cast this as a function. It is a function wit
[all...]
/seL4-l4v-master/graph-refine/
H A Dpseudo_compile.py7 # pseudo-compiler for use of aggregate types in C-derived function code
303 def compile_struct_use (function):
304 trace ('Compiling in %s.' % function.name)
305 vs = get_vars (function)
306 max_node = max (function.nodes.keys () + [2])
324 for n in function.nodes:
325 node = function.nodes[n]
339 function.inputs = expand_lval_list (replaces, function.inputs)
340 function
[all...]
/seL4-l4v-master/HOL4/src/coretypes/
H A DPairedLambda.sml121 (* Internal function: ITER_BETA_CONV (iterated, tupled beta-conversion).*)
128 (* LIST_BETA_CONV, but this function also does paired abstractions. *)
143 (* Internal function: ARGS_CONV (apply a list of conversions to the *)
144 (* arguments of a curried function application). *)
163 (* Internal function RED_WHERE. *)
165 (* Given the arguments "f" and "tm[f]", this function produces a *)
193 (* Internal function: REDUCE *)
195 (* This function does the appropriate beta-reductions in the result of *)
246 (* done component-wise, and function applications are effectively *)
/seL4-l4v-master/HOL4/examples/hardware/hol88/
H A Dbinary-trees.ml43 % Prove that the function NODE is one-to-one. %
70 % Define a height function on trees. %
76 % - false = don't make Height an infix function. %
/seL4-l4v-master/HOL4/Manual/Logic/
H A Dsyntax.tex135 \put(.5,1.5){\makebox(0,0)[b]{\footnotesize function types}}
182 \item {\bf Function types:}\index{function types, in HOL logic@function types, in \HOL{} logic!abstract form of} If $\sigma_1$
183 and $\sigma_2$ are types, then $\sigma_1\fun\sigma_2$ is the function
270 for each type constant $(\nu,n)$ an $n$-ary function
284 single set, but is rather a set-valued function, ${\cal
317 $\alpha\!s.\sigma$ over $\Omega$, define a function
327 projection function, which sends $(X_{1},\ldots,X_{n})\in{\cal U}^{n}$
330 \item If $\sigma$ is a function type\index{function type
[all...]
/seL4-l4v-master/HOL4/examples/dev/sw/examples/
H A Dfc_examples.sml8 (* Simple examples involving function calls *)
/seL4-l4v-master/HOL4/src/datatype/mutrec/examples/
H A Dexample.sml3 * and a simple mutually-recursive function for computing the variables
110 * A simple function for finding the variables in an expression of
158 appear in the same mutually recursive function definition, type
166 function (like allowing quantification for each conjunct).
/seL4-l4v-master/HOL4/src/portableML/
H A DRedblackmap.sig71 [app f m] applies function f to the entries (k, v) in m, in
75 [revapp f m] applies function f to the entries (k, v) in m, in
78 [foldl f e m] applies the folding function f to the entries (k, v)
81 [foldr f e m] applies the folding function f to the entries (k, v)
H A DRedblackset.sig82 [app f s] applies function f to the elements of s, in increasing
85 [revapp f s] applies function f to the elements of s, in decreasing
88 [foldl f e s] applies the folding function f to the entries of the
91 [foldr f e s] applies the folding function f to the entries of the
H A DUTF8Set.sig34 s. If there is no prefix of s in t, then the function returns NONE.

Completed in 286 milliseconds

1234567891011>>