Searched refs:functions (Results 1 - 25 of 695) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/graph-refine/example/
H A Dtarget.py9 from target_objects import target_dir, structs, functions, const_globals namespace
21 syntax.check_funs (functions)
24 #pseudo_compile.compile_funcs (functions)
27 #pseudo_compile.combine_function_duplicates (functions)
30 for f in functions:
35 if f2 in functions:
36 pair = logic.mk_pairing (functions, f, f2)
/seL4-l4v-10.1.1/graph-refine/loop-example/synth/
H A Dtarget.py9 from target_objects import target_dir, structs, functions, const_globals namespace
21 syntax.check_funs (functions)
24 #pseudo_compile.compile_funcs (functions)
27 #pseudo_compile.combine_function_duplicates (functions)
30 for f in functions:
35 if f2 in functions:
36 pair = logic.mk_pairing (functions, f, f2)
/seL4-l4v-10.1.1/graph-refine/seL4-example/
H A Dtarget.py9 from target_objects import target_dir, structs, functions namespace
41 pseudo_compile.compile_funcs (functions)
46 pairs = [(s, 'Kernel_C.' + s) for s in functions
47 if ('Kernel_C.' + s) in functions]
60 syntax.check_funs (functions)
/seL4-l4v-10.1.1/graph-refine/
H A Dinst_logic.py19 from target_objects import functions, trace, pairings, pre_pairings, printout namespace
84 if l_fname in functions:
86 assert r_fname not in functions
108 functions[l_fname] = l_fun
109 functions[r_fname] = r_fun
125 if functions[fname].entry:
144 assert not functions[fname].nodes
145 functions[fname].nodes[1] = call
146 functions[fname].entry = 1
151 if functions[fnam
[all...]
/seL4-l4v-10.1.1/HOL4/src/Boolify/src/
H A DEncode.sig4 (* Basically the same as Konrad Slind's code to generate size functions *)
/seL4-l4v-10.1.1/isabelle/src/Pure/PIDE/
H A Dprotocol_handlers.scala19 functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty)
32 (handlers - name, functions -- old_handler.functions.map(_._1))
33 case None => (handlers, functions)
40 val dups = for ((a, _) <- handler.functions if functions1.isDefinedAt(a)) yield a
41 if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
43 (handlers1 + (name -> handler), functions1 ++ handler.functions)
48 copy(handlers = handlers2, functions = functions2)
61 case Markup.Function(a) if functions.isDefinedAt(a) =>
62 try { functions(
[all...]
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/PIDE/
H A Dprotocol_handlers.scala19 functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty)
32 (handlers - name, functions -- old_handler.functions.map(_._1))
33 case None => (handlers, functions)
40 val dups = for ((a, _) <- handler.functions if functions1.isDefinedAt(a)) yield a
41 if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
43 (handlers1 + (name -> handler), functions1 ++ handler.functions)
48 copy(handlers = handlers2, functions = functions2)
61 case Markup.Function(a) if functions.isDefinedAt(a) =>
62 try { functions(
[all...]
/seL4-l4v-10.1.1/seL4/libsel4/arch_include/x86/sel4/arch/
H A Dsyscalls.h17 #include <sel4/arch/functions.h>
/seL4-l4v-10.1.1/graph-refine/loop-example/O1/
H A Dtarget.py9 from target_objects import target_dir, structs, functions, const_globals namespace
38 pseudo_compile.compile_funcs (functions)
41 syntax.check_funs (functions)
/seL4-l4v-10.1.1/graph-refine/loop-example/O2/
H A Dtarget.py10 from target_objects import target_dir, structs, functions, const_globals namespace
39 pseudo_compile.compile_funcs (functions)
42 syntax.check_funs (functions)
/seL4-l4v-10.1.1/HOL4/Manual/Reference/
H A Dentries-intro.tex4 in the \HOL{} system. These include: general-purpose functions, such
5 as functions for list processing, arithmetic, input/output, and
6 interface configuration; functions for processing the types and terms
H A Dpreface.tex19 functions, such as \ML\ functions for list processing, arithmetic,
20 input/output, and interface configuration; functions for processing the types
/seL4-l4v-10.1.1/isabelle/src/Doc/Tutorial/document/
H A Dadvanced0.tex22 %functions, how to define recursive functions over nested recursive datatypes
23 %and how to deal with partial functions.
26 %functions is overly complicated by the requirement of
27 %totality, you should ponder the alternatives. In a logic of partial functions,
46 %\index{functions!partial}
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Tutorial/document/
H A Dadvanced0.tex22 %functions, how to define recursive functions over nested recursive datatypes
23 %and how to deal with partial functions.
26 %functions is overly complicated by the requirement of
27 %totality, you should ponder the alternatives. In a logic of partial functions,
46 %\index{functions!partial}
/seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/
H A DcompilerLib.sig19 (* these functions expose the back-end functions *)
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/
H A Dacl2encodeLib.sig4 (* Functions are encoded using the translate_..._function functions, and *)
40 (* The translation of under-specified recursive functions (eg. SEG) is *)
69 (* This has the advantage that functions run must faster. However, ACL2 *)
84 (* However, if functions are translated using the destructors then the *)
93 (* Initialises a type so that functions over it can be translated to ACL2 *)
94 (* This generates the following functions: *)
96 (* The standard map and all functions, these can be viewed *)
99 (* These functions form the basis of the translation and may *)
118 (* These functions translate non-polymorphic definitions that do not use *)
135 (* The first of these functions shoul
[all...]
H A Dtutorial.ml9 (* We also load the example types and the example functions. *)
16 (* Simple functions: *)
20 (* We start by encoding simple functions, that is, functions that may be *)
22 (* only on functions that may be encoded across their entire range. *)
24 (* form, where mutually recursive functions are given as conjunctions. *)
26 (* Such functions are translated using the function: *)
30 (* functions and the second is the argument itself. *)
108 (* function creates recognition functions, suitable for export to ACL2, for *)
136 (* As rewrites for translated functions ar
[all...]
/seL4-l4v-10.1.1/HOL4/src/res_quan/Manual/
H A DMakefile31 tex: theorems functions
34 functions:
/seL4-l4v-10.1.1/HOL4/examples/miller/prob/
H A Dprob_pseudoTools.sml17 (* Simple ML functions to help find good parameters for the linear
/seL4-l4v-10.1.1/isabelle/src/Pure/Tools/
H A Dprint_operation.scala41 val functions = List(Markup.PRINT_OPERATIONS -> put _)
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Tools/
H A Dprint_operation.scala41 val functions = List(Markup.PRINT_OPERATIONS -> put _)
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/extract/
H A Dlisp_extractLib.sig6 (* main functions for extraction *)
/seL4-l4v-10.1.1/graph-refine/graph-to-graph/
H A Dbench.py21 from graph_refine.target_objects import functions, functions_by_tag namespace
153 functions = target_objects.functions
/seL4-l4v-10.1.1/HOL4/src/holyhammer/
H A DholyHammer.sig38 (* Main functions *)
41 (* saving results of the next functions in goaltac_cache *)
47 (* Other functions *)
/seL4-l4v-10.1.1/l4v/isabelle/src/HOL/Hahn_Banach/document/
H A Droot.tex45 normed spaces, continuous linear-forms, norm of functions and an order on
46 functions by domain extension. The second part contains some lemmas about the
47 supremum (w.r.t.\ the function order) and extension of non-maximal functions.

Completed in 211 milliseconds

1234567891011>>