/seL4-l4v-master/HOL4/examples/dev/sw/ |
H A D | UList.sml | 18 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 D | UList.sml | 18 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 D | UList.sml | 18 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 D | Map.sml | 9 val lookup : 'a map * IntInf.int -> 'a value
|
H A D | MutableMapFunctor.sml | 24 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 D | PureMap.sml | 25 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 D | Unify.sml | 13 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 D | hashtbl.h | 41 int lookup(const char *, hashData &) const;
|
/seL4-l4v-master/HOL4/examples/fun-op-sem/for/ |
H A D | for.sml | 22 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 D | cache.scala | 23 protected def lookup[A](x: A): Option[A] = 44 lookup(x) match {
|
/seL4-l4v-master/l4v/isabelle/src/Pure/General/ |
H A D | cache.scala | 23 protected def lookup[A](x: A): Option[A] = 44 lookup(x) match {
|
/seL4-l4v-master/HOL4/polyml/Tests/ |
H A D | RunTests.sml | 44 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 D | mlNearestNeighbor.sml | 91 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 D | ConstMapML.sig | 16 (* [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 D | fmspScript.sml | 9 (* 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 D | Ho_Net.sig | 16 val lookup : term -> 'a net -> 'a list value
|
/seL4-l4v-master/HOL4/examples/logic/ltl/ |
H A D | concrRepScript.sml | 31 (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 D | concrGBArepScript.sml | 884 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 D | sptreeScript.sml | 50 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 D | gfgScript.sml | 31 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 D | regexp_mapScript.sml | 74 `(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 D | simplifier_trace_window.scala | 90 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 D | simplifier_trace_window.scala | 90 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 D | term.scala | 143 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 D | term.scala | 143 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 {
|