Searched refs:pair (Results 1 - 25 of 314) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/src/coretypes/pair-Manual/
H A DMakefile2 # Make the manual for the "pair" library #
30 entries.tex theorems.tex *.ind pair.ps pair.pdf
36 echo "\chapter{ML Functions in the pair Library}" >entries.tex; \
47 ${MAKEINDEX} pair.idx
49 pair:
50 latex pair.tex
53 dvips pair.dvi -o
55 pdf: pair.ps
56 pdflatex pair
[all...]
H A Ddescription.tex5 the pair library, hereafter referred to as `the Software'.
36 \chapter{The pair Library}
38 This manual describes the use of the pair library.
39 The pair library has been provided to reduce the difficulty of reasoning
41 The pair library contains a version of every standard \HOL\ function
44 pair library provides paired equivalents:
169 The pair library also contains many functions for which there are no
175 you must load the pair library.
176 To load the pair library, issue the following command:
178 load_library `pair`;;
[all...]
/seL4-l4v-10.1.1/graph-refine/
H A Dgraph-refine.py35 def toplevel_check (pair, check_loops = True, report = False, count = None,
38 printout ('Testing Function pair %s' % pair)
43 for (tag, fname) in pair.funs.iteritems ():
45 printout ('Skipping %s, underspecified %s' % (pair, tag))
57 p = check.build_problem (pair)
101 trace ('EXCEPTION in handling %s:' % pair)
113 printout ('Result %s for pair %s, time taken: %.2fs'
114 % (result, pair, end_time - start_time))
124 pairs = list (set ([pair fo
[all...]
H A Dstats.py17 pairings_names = dict ([(pair.name, pair) for pair in pairings_set])
20 (_, nm) = line.split (' pair ', 1)
22 pair = pairings_names[nm]
25 proofs[pair] = pn
31 for (pair, proof) in proofs.iteritems ():
36 p = check.build_problem (pair)
142 print 'Search pair decay in random examples (idx, window size, trace):'
146 print 'Search pair deca
[all...]
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/
H A DILTheory.sml23 ((T"prod" "pair"
24 [T"MREG" "IL" [], T"prod" "pair" [alpha, T"MEXP" "IL" []]] -->
25 T"prod" "pair"
27 T"prod" "pair" [alpha, T"EXP" "preARM" []]]))),
32 [T"prod" "pair"
34 T"prod" "pair"
35 [T"prod" "pair" [T"num" "num" [], T"OFFSET" "preARM" []],
36 T"prod" "pair"
38 T"prod" "pair"
40 T"prod" "pair"
[all...]
/seL4-l4v-10.1.1/graph-refine/example/
H A Dtarget.py36 pair = logic.mk_pairing (functions, f, f2)
37 pairings[f] = [pair]
38 pairings[f2] = [pair]
/seL4-l4v-10.1.1/graph-refine/loop-example/synth/
H A Dtarget.py36 pair = logic.mk_pairing (functions, f, f2)
37 pairings[f] = [pair]
38 pairings[f2] = [pair]
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/
H A Dpairs.c137 SHORT {* creates an empty variable pair table *}
178 SHORT {* set one variable pair *}
179 PROTO {* int bdd_setpair(bddPair *pair, int oldvar, int newvar)
180 int bdd_setbddpair(bddPair *pair, BDD oldvar, BDD newvar) *}
181 DESCR {* Adds the pair {\tt (oldvar,newvar)} to the table of pairs
182 {\tt pair}. This results in {\tt oldvar} being substituted
195 int bdd_setpair(bddPair *pair, int oldvar, int newvar) argument
197 if (pair == NULL)
205 bdd_delref( pair->result[bddvar2level[oldvar]] );
206 pair
216 bdd_setbddpair(bddPair *pair, int oldvar, BDD newvar) argument
251 bdd_setpairs(bddPair *pair, int *oldvar, int *newvar, int size) argument
265 bdd_setbddpairs(bddPair *pair, int *oldvar, BDD *newvar, int size) argument
[all...]
/seL4-l4v-10.1.1/isabelle/src/Pure/ML/
H A Dml_syntax.scala49 /* pair */
51 def print_pair[A, B](f: A => String, g: B => String)(pair: (A, B)): String =
52 "(" + f(pair._1) + ", " + g(pair._2) + ")"
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/ML/
H A Dml_syntax.scala49 /* pair */
51 def print_pair[A, B](f: A => String, g: B => String)(pair: (A, B)): String =
52 "(" + f(pair._1) + ", " + g(pair._2) + ")"
/seL4-l4v-10.1.1/isabelle/src/Pure/
H A Dterm_xml.scala32 { case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) },
33 { case App(a, b) => (Nil, pair(term, term)(a, b)) }))
54 { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
55 { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/
H A Dterm_xml.scala32 { case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) },
33 { case App(a, b) => (Nil, pair(term, term)(a, b)) }))
54 { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
55 { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
/seL4-l4v-10.1.1/HOL4/src/real/
H A DrealLib.sig14 (* Incorporates simpsets for bool, pair, and arithmetic *)
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/examples/solitare/
H A Dsolitare.cxx19 bddPair *pair; // Renaming pair variable
130 // Make renaming pair and current state variables
133 pair = bdd_newpair();
135 bdd_setpair(pair, n*2+1, n*2);
156 next = bdd_replace(next, pair);
181 next = bdd_replace(next, pair);
/seL4-l4v-10.1.1/isabelle/src/Pure/PIDE/
H A Dprotocol.scala19 Some(pair(long, list(pair(long, list(long))))(Symbol.decode_yxml(text)))
370 Symbol.encode_yxml(list(pair(string, string))(table))
382 Symbol.encode_yxml(list(pair(string, properties))(lst))
410 (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
413 Symbol.encode_yxml(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
420 val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source))))
451 { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
458 pair(string, pair(strin
[all...]
H A Dcommand.scala39 { import XML.Encode._; list(pair(long, tree))(results.rep.toList) }
42 { import XML.Decode._; make(list(pair(long, tree))(body)) }
126 pair(bool, Symbol.Text_Chunk.encode_name)(index.status, index.chunk_name)
131 list(pair(markup_index, markup_tree))(markups.rep.toList)
140 val (status, chunk_name) = pair(bool, Symbol.Text_Chunk.decode_name)(body)
144 (Markups.empty /: list(pair(markup_index, Markup_Tree.from_XML(_)))(body))(_ + _)
236 pair(long, pair(string, pair(pair(lis
[all...]
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/PIDE/
H A Dprotocol.scala19 Some(pair(long, list(pair(long, list(long))))(Symbol.decode_yxml(text)))
370 Symbol.encode_yxml(list(pair(string, string))(table))
382 Symbol.encode_yxml(list(pair(string, properties))(lst))
410 (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
413 Symbol.encode_yxml(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
420 val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source))))
451 { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
458 pair(string, pair(strin
[all...]
H A Dcommand.scala39 { import XML.Encode._; list(pair(long, tree))(results.rep.toList) }
42 { import XML.Decode._; make(list(pair(long, tree))(body)) }
126 pair(bool, Symbol.Text_Chunk.encode_name)(index.status, index.chunk_name)
131 list(pair(markup_index, markup_tree))(markups.rep.toList)
140 val (status, chunk_name) = pair(bool, Symbol.Text_Chunk.decode_name)(body)
144 (Markups.empty /: list(pair(markup_index, Markup_Tree.from_XML(_)))(body))(_ + _)
236 pair(long, pair(string, pair(pair(lis
[all...]
/seL4-l4v-10.1.1/isabelle/src/Pure/General/
H A Dgraph_display.scala61 list(pair(pair(string, pair(string, x => x)), list(string)))(body)
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/
H A Dgraph_display.scala61 list(pair(pair(string, pair(string, x => x)), list(string)))(body)
/seL4-l4v-10.1.1/isabelle/src/Pure/Tools/
H A Dprint_operation.scala35 list(pair(string, string))(Symbol.decode_yxml(msg.text))
H A Dbuild.scala219 pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool,
220 pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
221 pair(strin
[all...]
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Tools/
H A Dprint_operation.scala35 list(pair(string, string))(Symbol.decode_yxml(msg.text))
/seL4-l4v-10.1.1/HOL4/src/0/
H A DKernelTypes.sml5 Elements in signatures are determined by a (name,theory) pair.
7 create more than one such pair, and they need to be distinguished).
47 The representation of theorems. A "tag" is a pair of the oracles
/seL4-l4v-10.1.1/HOL4/src/coretypes/
H A DpairSyntax.sml18 Type.mk_thy_type {Tyop = "prod", Thy = "pair", Args = [ty1, ty2]}
22 SOME{Tyop = "prod", Thy = "pair", Args = [ty1, ty2]} => (ty1, ty2)
35 val fst_tm = prim_mk_const {Name="FST", Thy="pair"}
36 val snd_tm = prim_mk_const {Name="SND", Thy="pair"}
37 val curry_tm = prim_mk_const {Name="CURRY", Thy="pair"}
38 val pair_map_tm = prim_mk_const {Name="##", Thy="pair"}
39 val lex_tm = prim_mk_const {Name="LEX", Thy="pair"}
40 val swap_tm = prim_mk_const {Name="SWAP", Thy="pair"}
41 val pair_case_tm = prim_mk_const {Name = "pair_CASE", Thy = "pair"}
44 Make a pair fro
[all...]

Completed in 212 milliseconds

1234567891011>>