Searched refs:lookup (Results 1 - 25 of 166) sorted by relevance

1234567

/seL4-l4v-master/HOL4/examples/dev/sw/
H A DUList.sml18 fun lookup _ [] = raise NotFound function
19 | lookup x ((y,z)::l) = if x=y then z else lookup x l
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/
H A DUList.sml18 fun lookup _ [] = raise NotFound function
19 | lookup x ((y,z)::l) = if x=y then z else lookup x l
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/util/
H A DUList.sml18 fun lookup _ [] = raise NotFound function
19 | lookup x ((y,z)::l) = if x=y then z else lookup x l
/seL4-l4v-master/HOL4/examples/l3-machine-code/lib/
H A DMap.sml9 val lookup : 'a map * IntInf.int -> 'a value
H A DMutableMapFunctor.sml24 fun lookup (Array a, v) = Array.sub (a, IntInf.toInt v) function
25 | lookup (Tree (s, d, t), v) =
67 val v = lookup (p, 1);
73 val v = lookup (p, 1);
H A DPureMap.sml25 fun lookup (Vector a, v) = Vector.sub (a, IntInf.toInt v) function
26 | lookup (VTree (s, d, t), v) =
68 val v = lookup (p, 1);
/seL4-l4v-master/HOL4/src/simp/src/
H A DUnify.sml13 fun lookup x [] = raise ERR "lookup" "not found" function
14 | lookup x ({redex,residue}::t) =
15 if aconv redex x then residue else lookup x t;
18 if is_var tm then lookup tm env handle HOL_ERR _ => tm
27 exists (fn fv => aconv fv v orelse f (lookup fv env)
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/examples/calculator/
H A Dhashtbl.h41 int lookup(const char *, hashData &) const;
/seL4-l4v-master/HOL4/examples/fun-op-sem/for/
H A Dfor.sml22 fun lookup y [] = NONE function
23 | lookup y ((x,v)::xs) = if y = x then SOME v else lookup y xs
26 (case lookup x s of
/seL4-l4v-master/isabelle/src/Pure/General/
H A Dcache.scala23 protected def lookup[A](x: A): Option[A] =
44 lookup(x) match {
/seL4-l4v-master/l4v/isabelle/src/Pure/General/
H A Dcache.scala23 protected def lookup[A](x: A): Option[A] =
44 lookup(x) match {
/seL4-l4v-master/HOL4/polyml/Tests/
H A DRunTests.sml44 fun lookup s = function
51 { lookup = lookup, enter = enter, all = all }
64 lookupFix = #lookup fixSpace,
65 lookupSig = #lookup sigSpace,
66 lookupVal = #lookup valSpace,
67 lookupType = #lookup typeSpace,
68 lookupFunct = #lookup funSpace,
69 lookupStruct = #lookup strSpace,
/seL4-l4v-master/HOL4/src/AI/machine_learning/
H A DmlNearestNeighbor.sml91 fun dep_call_g rl lookup loopd gn =
92 if HOLset.member (loopd,gn) orelse not (can lookup gn) then () else
95 val (loc,call) = lookup gn
99 app (dep_call_g rl lookup newloopd) gnl
105 fun lookup x = ((thy,thmn,x), dfind (thy,thmn,x) calld) function
108 app (dep_call_g rl lookup loopd) ogl;
/seL4-l4v-master/HOL4/src/emit/
H A DConstMapML.sig16 (* [apply] peforms a lookup and returns the most specific match. Thus,
25 [exact_peek] does an exact lookup on the term. Thus, if you have the
/seL4-l4v-master/HOL4/src/transfer/
H A DfmspScript.sml9 (* wf sp /\ *) !a n. AN a n ==> OPTREL BC (FLOOKUP fm a) (lookup n sp)���;
15 rename [���OPTREL BC (FLOOKUP fm a) (lookup n sp)���] >> pop_assum mp_tac >>
16 map_every Cases_on [���FLOOKUP fm a���, ���lookup n sp���] >>
37 rename [���FLOOKUP (fm |+ (k1,v)) k2���, ���lookup m (insert n spv sp)���] >>
49 rename [���lookup _ sp���] >>
51 FUN_FMAP (\a. @b. BC b (THE (lookup (@n. AN a n) sp)))
103 ���option_CASE (lookup n sp1)���] >>
119 rename [���FLOOKUP (fm \\ k1) k2���, ���lookup m (delete n sp)���] >>
/seL4-l4v-master/HOL4/src/1/
H A DHo_Net.sig16 val lookup : term -> 'a net -> 'a list value
/seL4-l4v-master/HOL4/examples/logic/ltl/
H A DconcrRepScript.sml31 (IMAGE (\n. lookup n graph.nodeInfo) (domain graph.nodeInfo))}`;
38 MEM x (CAT_OPTIONS (MAP (\n. lookup n graph.nodeInfo) l)) })
44 (IMAGE (\n. lookup n graph.nodeInfo) (domain graph.nodeInfo))
520 lookup nId graph.followers
533 ��� SOME suc = lookup sucId graph.nodeInfo
667 ``!g id node f. unique_node_formula g ��� (lookup id g.nodeInfo = SOME node)
694 (lookup id g.nodeInfo = SOME q)
695 ��� (lookup id g.followers = SOME fls)
696 ��� (lookup sucId g.nodeInfo = SOME suc)
713 lookup nI
[all...]
H A DconcrGBArepScript.sml884 case lookup aa_id g_AA.followers of
891 case lookup id g_AA.nodeInfo of
909 in do node <- lookup aa_id g_AA.nodeInfo ;
925 >> Cases_on `lookup x g_AA.followers` >> fs[]
933 case lookup id g_AA.nodeInfo of
952 >> Cases_on `lookup id g_AA.nodeInfo` >> fs[]
953 >> rename[`lookup id g_AA.nodeInfo = SOME node`]
967 ==> case lookup id g_AA.followers of
971 ��� (lookup id g_AA.nodeInfo = SOME n)
974 rpt strip_tac >> fs[] >> Cases_on `lookup i
[all...]
/seL4-l4v-master/HOL4/src/finite_maps/
H A DsptreeScript.sml50 val lookup_def = tzDefine "lookup" `
51 (lookup k LN = NONE) /\
52 (lookup k (LS a) = if k = 0 then SOME a else NONE) /\
53 (lookup k (BN t1 t2) =
55 else lookup ((k - 1) DIV 2) (if EVEN k then t1 else t2)) /\
56 (lookup k (BS t1 a t2) =
58 else lookup ((k - 1) DIV 2) (if EVEN k then t1 else t2))
148 ``!k a t. lookup k (insert k a t) = SOME a``,
177 ``!k2 v t k1. lookup k1 (insert k2 v t) =
178 if k1 = k2 then SOME v else lookup k
[all...]
/seL4-l4v-master/HOL4/examples/generic_finite_graphs/
H A DgfgScript.sml31 followers_old <- lookup src g.followers;
32 preds_old <- lookup tgt g.preds;
55 ���k nl e n. lookup k adjmap = SOME nl ��� MEM (e,n) nl ���
89 >- (rename[`lookup k (insert i _ _) = SOME nl`, `MEM (e',n) nl`,
93 >- (rename[`lookup k1 (insert k2 _ _) = SOME nl`, `MEM (e',n) nl`,
/seL4-l4v-master/HOL4/examples/formal-languages/regular/
H A Dregexp_mapScript.sml74 `(fdom cmp bmap = {a | ?x. lookup cmp a bmap = SOME x}) /\
75 (frange cmp bmap = {x | ?a. lookup cmp a bmap = SOME x})`;
128 !x. lookup cmp x bmap = FLOOKUP (to_fmap cmp bmap) {x}
137 ==> (lookup cmp b (insert cmp a y bmap) = SOME y)
148 ==> (lookup cmp b (insert cmp a y bmap) = lookup cmp b bmap)
159 (lookup cmp b (insert cmp a y bmap) =
162 else lookup cmp b bmap)
171 (lookup cmp x (bmap_of_list cmp fmap list) = SOME (fmap ' x))
183 (lookup cm
[all...]
/seL4-l4v-master/isabelle/src/Tools/jEdit/src/
H A Dsimplifier_trace_window.scala90 def walk_trace(rest: List[Simplifier_Trace.Item.Data], lookup: Map[Long, Trace_Tree]): Unit =
95 lookup.get(head.parent) match {
108 walk_trace(tail, lookup)
118 walk_trace(tail, lookup)
125 walk_trace(tail, lookup + (head.serial -> entry))
/seL4-l4v-master/l4v/isabelle/src/Tools/jEdit/src/
H A Dsimplifier_trace_window.scala90 def walk_trace(rest: List[Simplifier_Trace.Item.Data], lookup: Map[Long, Trace_Tree]): Unit =
95 lookup.get(head.parent) match {
108 walk_trace(tail, lookup)
118 walk_trace(tail, lookup)
125 walk_trace(tail, lookup + (head.serial -> entry))
/seL4-l4v-master/isabelle/src/Pure/
H A Dterm.scala143 lookup(x) getOrElse store(Indexname(cache_string(x.name), x.index))
146 if (x.isEmpty) Nil else lookup(x) getOrElse store(x.map(cache_string(_)))
152 lookup(x) match {
167 lookup(x) match {
176 lookup(x) match {
195 lookup(x) match {
/seL4-l4v-master/l4v/isabelle/src/Pure/
H A Dterm.scala143 lookup(x) getOrElse store(Indexname(cache_string(x.name), x.index))
146 if (x.isEmpty) Nil else lookup(x) getOrElse store(x.map(cache_string(_)))
152 lookup(x) match {
167 lookup(x) match {
176 lookup(x) match {
195 lookup(x) match {

Completed in 347 milliseconds

1234567