/seL4-l4v-master/HOL4/src/integer/testing/ |
H A D | readproblemfile.sig | 16 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 D | Cache.sig | 17 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 D | Sequence.sml | 15 (*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 D | Holmake_types.sig | 48 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 D | IO.sml | 24 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 D | selftest.sml | 23 fun normalForms_test (fname, function :conv, problem, result) = let 33 function (* 'b -> 'a *)
|
H A D | folMapping.sig | 20 {higher_order : bool, (* Application is a first-order function *)
|
/seL4-l4v-master/l4v/tools/c-parser/testfiles/ |
H A D | parse_complit.c | 57 int function(void) function
|
/seL4-l4v-master/HOL4/src/datatype/mutrec/ |
H A D | MutRecDef.sml | 33 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 D | FactScript.sml | 65 (* 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 D | Sol_ranges.sml | 32 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 D | Exists_arith.sml | 32 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 D | Solve.sml | 26 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 D | PmatchHeuristics.sig | 63 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 D | Mutual.sml | 26 (* 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 D | CODETREE_CODEGEN_CONSTANT_FUNCTIONS.sml | 19 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 D | pseudo_compile.py | 7 # 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 D | PairedLambda.sml | 121 (* 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 D | binary-trees.ml | 43 % 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 D | syntax.tex | 135 \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 D | fc_examples.sml | 8 (* Simple examples involving function calls *)
|
/seL4-l4v-master/HOL4/src/datatype/mutrec/examples/ |
H A D | example.sml | 3 * 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 D | Redblackmap.sig | 71 [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 D | Redblackset.sig | 82 [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 D | UTF8Set.sig | 34 s. If there is no prefix of s in t, then the function returns NONE.
|