/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Rule.sig | 59 val subtermsConv : conv -> conv (* All function arguments *) 175 val functionCongruence : Term.function -> Thm.thm
|
H A D | Atom.sig | 50 (* A total comparison function for atoms. *)
|
H A D | PortableMosml.sml | 54 (* Timing function applications. *)
|
/seL4-l4v-master/isabelle/src/Doc/Tutorial/document/ |
H A D | basics.tex | 122 \item[function types,]\index{function types} 133 function. 154 applying functions to arguments. If \isa{f} is a function of type 175 \isa{\isasymlambda{}x.~x+1} is the function that takes an argument \isa{x} and 192 Equality\index{equality} is available in the form of the infix function 222 important overloaded function symbols. 231 Isabelle allows infix functions like \isa{+}. The prefix form of function
|
H A D | advanced0.tex | 32 %proof time. In HOL you may have to work hard to define a function, but proofs
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Rule.sig | 59 val subtermsConv : conv -> conv (* All function arguments *) 175 val functionCongruence : Term.function -> Thm.thm
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Tutorial/document/ |
H A D | basics.tex | 122 \item[function types,]\index{function types} 133 function. 154 applying functions to arguments. If \isa{f} is a function of type 175 \isa{\isasymlambda{}x.~x+1} is the function that takes an argument \isa{x} and 192 Equality\index{equality} is available in the form of the infix function 222 important overloaded function symbols. 231 Isabelle allows infix functions like \isa{+}. The prefix form of function
|
/seL4-l4v-master/HOL4/examples/fun-op-sem/cbv-lc/ |
H A D | typesScript.sml | 26 (* Get the size function generated by the call to Datatype *) 56 (* Define a helper function for the termination argument below. *)
|
/seL4-l4v-master/HOL4/src/opentheory/reader/ |
H A D | OpenTheoryReader.sig | 43 An axiom function for readers that tries to find the desired theorem in the 57 current theory. The first argument to [define_const_in_thy] is a function to
|
/seL4-l4v-master/HOL4/examples/fun-op-sem/small-step/ |
H A D | determSemScript.sml | 24 * - a step function (to an option for representing stuckness), 59 * - a evaluation function
|
/seL4-l4v-master/HOL4/src/postkernel/ |
H A D | Theory.sig | 81 already been stored. The set_theory_data function overrides whatever 127 (* Theory files (which are just SML source code) call this function as
|
/seL4-l4v-master/HOL4/src/compute/src/ |
H A D | compute_rules.sml | 19 fun RULES_ERR function message = 21 origin_function = function,
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/X86Code/ |
H A D | X86FOREIGNCALL.sml | 57 rbx, rbp, rdi, rsi, rsp, r12-r15 are saved by the called function. 59 ebx, edi, esi, ebp and esp are saved by the called function. 330 CallAddress(RegisterArg entryPtrReg), (* Call the function *) 338 (* Since this is an ML function we need to remove any ML stack arguments. *) 403 version we make this a function. *) 456 (* Build a foreign call function. The arguments are the abi, the list of argument types and the result type. 457 The result is the code of the ML function that takes three arguments: the C function to call, the arguments 484 | (CTypeVoid, _) => raise Foreign.Foreign "Void cannot be used for a function argument" 560 (* Adjustment to be made when the function return [all...] |
/seL4-l4v-master/isabelle/src/Doc/Logics/document/ |
H A D | CTT.tex | 115 \index{*"` symbol}\index{function applications!in CTT} 119 \tt ` & $[i,i]\to i$ & Left 55 & function application\\ 135 \rm function space $A\to B$ \\ 170 the function application operator (sometimes called `apply'), and the 2-place 173 \hbox{\tt lam $x$. $b$} and $b{\tt`}a$. A CTT function~$f$ is simply an 424 it can even express Ackermann's function, which is not primitive recursive 428 include function types as a special case. The rules correspond to the 722 the predecessor function is $\lambda v. {\tt rec}(v, 0, \lambda x\,y. x)$. 757 predecessor function on the natural numbers. 799 $\prod@{x\in N}N$, which is shown as the function typ [all...] |
/seL4-l4v-master/l4v/isabelle/src/Doc/Logics/document/ |
H A D | CTT.tex | 115 \index{*"` symbol}\index{function applications!in CTT} 119 \tt ` & $[i,i]\to i$ & Left 55 & function application\\ 135 \rm function space $A\to B$ \\ 170 the function application operator (sometimes called `apply'), and the 2-place 173 \hbox{\tt lam $x$. $b$} and $b{\tt`}a$. A CTT function~$f$ is simply an 424 it can even express Ackermann's function, which is not primitive recursive 428 include function types as a special case. The rules correspond to the 722 the predecessor function is $\lambda v. {\tt rec}(v, 0, \lambda x\,y. x)$. 757 predecessor function on the natural numbers. 799 $\prod@{x\in N}N$, which is shown as the function typ [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw2/test/ |
H A D | regAllocTest.sml | 10 (* Test case 1: The factorial function. *)
|
/seL4-l4v-master/HOL4/src/0/ |
H A D | Subst.sml | 85 * Composition of 2 substitution. We need to provide a function [mk_cl] that
|
/seL4-l4v-master/HOL4/src/compute/examples/ |
H A D | Arith.sml | 40 * function strongly.
|
/seL4-l4v-master/HOL4/src/datatype/mutrec/examples/ |
H A D | var_example.sml | 75 (* A simple function for finding the variables in a program *)
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibMultiset.sml | 72 prevents this function being implemented :-(
|
/seL4-l4v-master/HOL4/developers/mlton-srcs/ |
H A D | Binarymap.sml | 50 [app f m] applies function f to the entries (k, v) in m, in 54 [revapp f m] applies function f to the entries (k, v) in m, in 57 [foldl f e m] applies the folding function f to the entries (k, v) 60 [foldr f e m] applies the folding function f to the entries (k, v)
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ |
H A D | COMPILERBODYSIG.sml | 59 Returns the parse tree and, if successful, a function that executes the
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
H A D | BaseParseTreeSig.sml | 220 (* A function binding is a list of clauses, each of which uses a 221 valBinding to hold the list of patterns and the corresponding function 222 body. The second pass extracts the function variable and the number of 235 and fvalclause = (* Clause within a function binding. *)
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | Option.sml | 21 (* G&R 2004 status: updated, added "app" function. *)
|
H A D | RealArray.sml | 26 function to load and store reals although it would probably be
|