Searched refs:function (Results 51 - 75 of 876) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/
H A DBaseCodeTreeSig.sml63 (* Applied as a function - the list is where the result goes, the codetree list
77 | Eval of (* Evaluate a function with an argument list. *)
79 function: codetree,
100 | BeginLoop of (* Start of tail-recursive inline function. *)
103 | Loop of (codetree * argumentType) list (* Jump back to start of tail-recursive function. *)
140 inline function. Tuple entries are functions from an integer
141 offset to one of these pairs; inline function entries are a
168 body : codetree, (* The body of the function. *)
173 resultType : argumentType, (* Result "type" of the function. *)
175 recUse : codeUse list (* Recursive use of the function *)
[all...]
H A DBaseCodeTree.sml48 (* Applied as a function - the list is where the result goes, the codetree list
62 | Eval of (* Evaluate a function with an argument list. *)
64 function: codetree,
85 | BeginLoop of (* Start of tail-recursive inline function. *)
88 | Loop of (codetree * argumentType) list (* Jump back to start of tail-recursive function. *)
131 inline function. Tuple entries are functions from an integer
132 offset to one of these pairs; inline function entries are a
138 includes a function from int, the index, to the (general, special) pair
140 reason is that if we have a function that contains a reference to, say a tuple,
141 in its closure we can pass in a EnvSpecTuple entry with a function tha
[all...]
H A DCODETREE_STATIC_LINK_AND_CASES.sml46 (* Property tag to indicate which arguments to a function are functions
65 is a function a closure must be made for it. *)
107 fun insert(Eval { function = Extract LoadRecursive, argList, resultType, ...}) =
120 (* If we are calling a function which has been declared this
122 function would. *)
123 BICEval {function = BICExtract func, argList = newargs, resultType=resultType}
126 | insert(Eval { function = Extract ext, argList, resultType, ...}) =
141 (* If we are calling a function which has been declared this
143 function would. *)
144 BICEval {function
[all...]
/seL4-l4v-master/HOL4/examples/acl2/ml/
H A DpolytypicLib.sig14 type function = type
129 (* Split function definition *)
138 (* The function and theorem database *)
144 val get_translation_precise : hol_type -> hol_type -> (string,function) dict ref
145 val get_translation : hol_type -> hol_type -> (string,function) dict ref
157 val get_coding_function_precise : hol_type -> hol_type -> string -> function
158 val get_coding_function : hol_type -> hol_type -> string -> function
165 val add_coding_function_precise : hol_type -> hol_type -> string -> function -> unit
166 val add_coding_function : hol_type -> hol_type -> string -> function -> unit
169 val get_source_function_precise : hol_type -> string -> function
[all...]
/seL4-l4v-master/HOL4/examples/computability/lambda/
H A DHaltingProblemsScript.sml18 done by saying something like there is no computable function for
25 the ��-calculus setting, the cDB function is the function that
27 encoding the function.
94 (* Impossibility of determining whether or not arbitrary function applied
112 Needs the computability of the encoding function cDB. *)
/seL4-l4v-master/HOL4/examples/dev/Fact32/
H A DFact32.ml51 (* We implement multiplication with a naive iterative multiplier function *)
71 (* Implement iterative function as a step to implementing factorial *)
82 (* Implement a function Fact32 to compute SND(Fact32Iter (n,1)) *)
/seL4-l4v-master/HOL4/src/num/arith/Manual/
H A Ddescription.tex4 for the HOL system~\cite{description}. The main function is a partial decision
10 The main function, \ml{ARITH\_CONV}, is a partial decision procedure for
18 contain variables are not included in the subset, but the function
33 The function makes use of a number of preprocessors\index{preprocessors} which
36 the predecessor function {\small\verb%PRE%}, and conditional
37 statements\index{conditional statements} can be eliminated using the function
40 of universally quantified formulae to be accepted. There is also a function
47 The main function, \ml{ARITH\_CONV}, is constructed from two separate
78 function \ml{load\_library}\index{load\_library@{\ptt load\_library}} (see the
124 It is easy to define a function whic
[all...]
/seL4-l4v-master/HOL4/src/res_quan/src/
H A DCond_rewrite.sml15 fun COND_REWR_ERR {function,message} =
17 origin_function = function,
114 then raise COND_REWR_ERR{function="MATCH_SUBS1",
151 (* fn is a search function which returns a list of matches in the format *)
152 (* of the list returned by the system function match. *)
158 (* This tactic uses the search function fn to find any matches of Q in *)
181 then raise COND_REWR_ERR{function="COND_REWR_TAC", message="no match"}
189 (raise COND_REWR_ERR {function="COND_REWR_TAC",
249 (* fn is a function attempting to match the lhs of the conclusion of th *)
251 (* this function i
[all...]
/seL4-l4v-master/HOL4/examples/CCS/
H A DObsCongrLib.sml42 (* Define the function OC_THENC. *)
49 (* Define the function OC_ORELSEC. *)
53 (* Define the function OC_REPEATC. *)
H A DWeakEQLib.sml40 (* Define the function OE_THENC. *)
47 (* Define the function OE_ORELSEC. *)
51 (* Define the function OE_REPEATC *)
/seL4-l4v-master/l4v/isabelle/src/HOL/Data_Structures/document/
H A Droot.tex45 The insert function follows Okasaki \cite{Okasaki}. The delete function
47 an alternative delete function is given in theory \isa{RBT\_Set2}.
/seL4-l4v-master/isabelle/src/HOL/Data_Structures/document/
H A Droot.tex45 The insert function follows Okasaki \cite{Okasaki}. The delete function
47 an alternative delete function is given in theory \isa{RBT\_Set2}.
/seL4-l4v-master/HOL4/examples/dev/
H A DFact.ml33 (* To implement multiplication we use a naive iterative multiplier function *)
52 (* Implement iterative function as a step to implementing factorial *)
62 (* Implement a function Fact to compute SND(FactIter (n,1)) *)
147 (* Verify Fact is indeed the factorial function *)
/seL4-l4v-master/HOL4/src/1/
H A Dfastbuild.sml4 (* (and store_thm) function to be a call to mk_thm, so proofs that require *)
/seL4-l4v-master/HOL4/src/parse/
H A Dterm_tokens.sig14 (* NONE indicates end of input; this function *always* advances over
/seL4-l4v-master/HOL4/src/portableML/poly/
H A DIntset.sig68 [app f s] applies function f to the elements of s, in increasing
71 [revapp f s] applies function f to the elements of s, in decreasing
74 [foldl f e s] applies the folding function f to the entries of the
77 [foldr f e s] applies the folding function f to the entries of the
/seL4-l4v-master/HOL4/src/quantHeuristics/
H A DquantHeuristicsLibFunRemove.sig11 (* very simple for to state that some function can be remove.
H A DquantHeuristicsLibSimple.sig32 (* A simple_guess_seaech_fun is a function that searches a guess. Given a
53 function.
75 (* to find guesses for equations, a function can also be applied to
80 function to apply, a check when to apply and a theorem about how
/seL4-l4v-master/HOL4/tools/
H A Dbuildutils.sig43 (* applies function to every .sml and .sig file in given
72 Holmake, using function extras to generate extra commandline
73 arguments, and function analysis to generate extra
78 The sysl function actually does the invocation (fork/exec,
/seL4-l4v-master/HOL4/src/AI/sml_inspection/
H A DsmlParallel.sig20 function : 'a -> 'b -> 'c,
/seL4-l4v-master/HOL4/src/holyhammer/
H A DholyHammer.sig21 This function is used inside the tactictoe evaluation framework. *)
/seL4-l4v-master/HOL4/src/datatype/mutrec/utils/
H A DelsaUtils.sml33 fun UTILSLIB_ERR{function,message} =
35 origin_function = function,
63 {function = "find_match",
87 | mapshape _ = raise UTILSLIB_ERR{function = "mapshape",
237 {function = "FALSITY_INTRO",
283 {function = "SUPPOSE_TAC",
286 {function = "SUPPOSE_TAC",
310 {function = "REV_SUPPOSE_TAC",
313 {function = "REV_SUPPOSE_TAC",
431 {function
[all...]
/seL4-l4v-master/HOL4/tools/Holmake/
H A Dinternal_functions.sml57 raise Fail "empty from argument to `subst' function"
300 raise Fail "Bad number of arguments to `if' function."
311 raise Fail "Bad number of arguments to `subst' function."
322 raise Fail "Bad number of arguments to `patsubst' function."
332 raise Fail "Bad number of arguments to `protect' function."
336 raise Fail "Bad number of arguments to 'dprot' function."
340 \function."
351 raise Fail "Bad number of arguments to 'which' function"
358 raise Fail "Bad number of arguments to 'wildcard' function"
366 raise Fail "Bad number of arguments to 'shell' function"
[all...]
/seL4-l4v-master/HOL4/examples/hardware/hol88/mos-count/
H A Dmos.ml7 % Not is a negation function in the four-valued %
8 % logic and U is the least upper bound function. %
/seL4-l4v-master/HOL4/src/finite_maps/
H A Dalist_treeLib.sig35 Adds a function's representation.
40 - a function g in the repr set.

Completed in 268 milliseconds

1234567891011>>