Searched refs:filter (Results 1 - 25 of 578) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/src/metis/
H A DmlibClauseset.sig12 type filter = {subsumption : bool, simplification : int, splitting : bool} type
13 type parameters = {prefactoring : filter, postfactoring : filter}
16 val update_subsumption : (bool -> bool) -> filter -> filter
17 val update_simplification : (int -> int) -> filter -> filter
18 val update_splitting : (bool -> bool) -> filter -> filter
19 val update_prefactoring : (filter
[all...]
H A DmlibLiteralnet.sml70 fun filter pred = function
72 fun filt (_,l) = let val l = List.filter pred l in (length l, l) end
75 ((T.filter pred pos, T.filter pred neg), (filt t, filt f))
H A DmlibSubsume.sml29 val ofilter = Option.filter;
138 fun filter pred (SUBSUME {zero,one,many}) = function
142 val zero = S.filter (pred o snd) zero
143 val one = N.filter (pred o snd) one
146 val l = N.filter (not o curry I.member h o fst) l
147 val r = N.filter (not o curry I.member h o fst) r
/seL4-l4v-master/HOL4/src/simp/src/
H A DpureSimps.sml12 filter = SOME Cond_rewr.mk_cond_rewrs,
H A DcombinSimps.sml6 name = SOME "COMBIN", convs = [], congs = [], filter = NONE, ac = [],
H A DboolSimps.sml35 rewrs = [], congs = [], filter = NONE, ac = [], dprocs = []}
52 ac = [], congs = [literal_cong], convs = [], filter = NONE,
86 congs = [literal_cong], filter = NONE, ac = [], dprocs = []};
100 convs = [], rewrs = [], filter=NONE, ac=[], dprocs=[]}
110 rewrs = [], filter= NONE, ac = [], dprocs=[]
150 rewrs=[],filter=NONE,ac=[],dprocs=[],congs=[]};
167 ac = [], congs = [let_cong], convs = [], filter = NONE,
273 dprocs = [], filter = NONE,
289 dprocs = [], filter = NONE,
309 convs = [], dprocs = [], filter
[all...]
/seL4-l4v-master/HOL4/tools/quote-filter/
H A Dselftest.sml3 val _ = system "./quote-filter input temp-output"
H A Dmlton-quote-filter.sml2 open filter.UserDeclarations
5 val lexer = filter.makeLexer input state
/seL4-l4v-master/HOL4/examples/acl2/lisp/obsolete/
H A Dfilter-forms.csh5 set pprint_book = ${ACL2_HOL_LISP}/filter-forms
/seL4-l4v-master/l4v/camkes/glue-spec/document/imgs/
H A DMakefile17 default: echo.pdf filter.pdf thydeps.pdf
/seL4-l4v-master/HOL4/examples/hardware/hol88/
H A Dquicksort.ml31 [(\(x.l'). filter(curry $> x) l');
32 (\(x.l'). filter($not o (curry $> x)) l')]);;
59 [(\(x.l'). filter(curry $> x) l');
60 (\(x.l'). filter($not o (curry $> x)) l')])
/seL4-l4v-master/HOL4/examples/l3-machine-code/lib/
H A DSet.sml15 fun diff (s1, s2) = List.filter (fn x => not (mem (x, s2))) s1
16 fun intersect (s1, s2) = List.filter (fn x => mem (x, s2)) s1
/seL4-l4v-master/HOL4/src/1/
H A DLVTermNetFunctorApplied.sml11 fun filter P s = function
/seL4-l4v-master/HOL4/examples/miller/prob/
H A Dprob_canonTools.sml16 filter = NONE,
/seL4-l4v-master/HOL4/src/tfl/src/test/
H A Dtfl_examplesScript.sml53 val _ = overload_on("filter", ``FILTER``)
59 qsort(ord,filter($~ o ord x) rst)++[x]++qsort(ord,filter(ord x) rst))`;
98 let ((L1,L2),P) = ((filter($~ o ord x) rst,
99 filter (ord x) rst),
129 ``LENGTH (filter (\y. SUC x <= y) L) <= LENGTH (filter (\y. x <= y) L)``,
134 WF_REL_TAC `measure \(x,L). LENGTH(filter (\y. x <= y) L)` THEN
139 Q.EXISTS_TAC `LENGTH (filter (\y. x <= y) L)` THEN
/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DAtomNet.sml40 val filter = TermNet.filter; value
H A DLiteralNet.sml44 fun filter pred {positive,negative} = function
45 {positive = AtomNet.filter pred positive,
46 negative = AtomNet.filter pred negative};
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DAtomNet.sml40 val filter = TermNet.filter; value
H A DLiteralNet.sml44 fun filter pred {positive,negative} = function
45 {positive = AtomNet.filter pred positive,
46 negative = AtomNet.filter pred negative};
/seL4-l4v-master/HOL4/examples/unification/triangular/nominal/
H A DntermLib.sml7 congs = [], filter = NONE,
16 congs = ths, filter = NONE,
/seL4-l4v-master/HOL4/examples/machine-code/compiler/
H A Dreg_allocLib.sml37 | all_distinct (x::xs) = x :: all_distinct (filter (fn y => x !~ y) xs)
42 fun diff xs ys = filter (fn y => not (mem y ys)) xs
43 fun intersect xs ys = filter (fn y => mem y xs) ys
80 val vs = filter (fn x => type_of x = ``:word32``) (free_vars tm)
88 val vs = filter (fn x => type_of x = ``:word32``) (free_vars tm)
107 fun partition p xs = filter p xs @ filter (not o p) xs
150 (filter (fn x => not (mem x [#"0",#"1",#"2",#"3",#"4",#"5",#"6",#"7",#"8",#"9",#"'"])) (tl ii) = [])
192 val xs = filter (fn x => x !~ subst m x) (dest_tuple tm)
199 val aux = filter (f
[all...]
/seL4-l4v-master/isabelle/src/Pure/Thy/
H A Dlatex.scala160 @tailrec def filter(lines: List[String], result: List[(String, Position.T)])
167 filter(rest1, (Exn.cat_message(msg1, msg2), pos) :: result)
169 filter(rest, (msg, Position.none) :: result)
170 case _ :: rest => filter(rest, result)
175 filter(Line.logical_lines(root_log), Nil)
/seL4-l4v-master/l4v/isabelle/src/Pure/Thy/
H A Dlatex.scala160 @tailrec def filter(lines: List[String], result: List[(String, Position.T)])
167 filter(rest1, (Exn.cat_message(msg1, msg2), pos) :: result)
169 filter(rest, (msg, Position.none) :: result)
170 case _ :: rest => filter(rest, result)
175 filter(Line.logical_lines(root_log), Nil)
/seL4-l4v-master/HOL4/examples/ARM/v4/
H A Darm_rulesLib.sml112 filter (fn x => substring(fst x, 0, 3) = "ARM") (theorems "arm_rules");
114 fun RULE_FIND m l = filter (can (MATCH_ARM_RULE m)) l;
116 fun RULE_GET m l = filter (fn x => not (term_eq (concl x) T))
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/ppc/
H A Dppc_encodeLib.sml47 val (_,(y,z)) = hd (filter (fn y => (fst y = x)) instructions)
59 | all_distinct (x::xs) = x::all_distinct (filter (fn y => not ((x:string) = y)) xs)
61 val i = filter (fn x => not (mem x ["bt","bf"])) i

Completed in 287 milliseconds

1234567891011>>