/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | BaseCodeTreeSig.sml | 63 (* 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 D | BaseCodeTree.sml | 48 (* 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 D | CODETREE_STATIC_LINK_AND_CASES.sml | 46 (* 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 D | polytypicLib.sig | 14 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 D | HaltingProblemsScript.sml | 18 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 D | Fact32.ml | 51 (* 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 D | description.tex | 4 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 D | Cond_rewrite.sml | 15 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 D | ObsCongrLib.sml | 42 (* Define the function OC_THENC. *) 49 (* Define the function OC_ORELSEC. *) 53 (* Define the function OC_REPEATC. *)
|
H A D | WeakEQLib.sml | 40 (* 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 D | root.tex | 45 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 D | root.tex | 45 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 D | Fact.ml | 33 (* 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 D | fastbuild.sml | 4 (* (and store_thm) function to be a call to mk_thm, so proofs that require *)
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | term_tokens.sig | 14 (* NONE indicates end of input; this function *always* advances over
|
/seL4-l4v-master/HOL4/src/portableML/poly/ |
H A D | Intset.sig | 68 [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 D | quantHeuristicsLibFunRemove.sig | 11 (* very simple for to state that some function can be remove.
|
H A D | quantHeuristicsLibSimple.sig | 32 (* 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 D | buildutils.sig | 43 (* 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 D | smlParallel.sig | 20 function : 'a -> 'b -> 'c,
|
/seL4-l4v-master/HOL4/src/holyhammer/ |
H A D | holyHammer.sig | 21 This function is used inside the tactictoe evaluation framework. *)
|
/seL4-l4v-master/HOL4/src/datatype/mutrec/utils/ |
H A D | elsaUtils.sml | 33 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 D | internal_functions.sml | 57 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 D | mos.ml | 7 % 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 D | alist_treeLib.sig | 35 Adds a function's representation. 40 - a function g in the repr set.
|