Searched refs:list (Results 251 - 275 of 1918) sorted by relevance

<<11121314151617181920>>

/seL4-l4v-10.1.1/HOL4/src/metis/
H A DfolMapping.sig16 type vars = term list * hol_type list
28 val hol_literals_to_fol : parameters -> vars * term list -> formula1 list
35 type Pattern = vars * term list
36 type Result = vars * thm list
37 val fol_thms_to_hol : parameters -> Axioms -> Pattern -> thm1 list -> Result
H A DmlibParser.sig26 val many : ('a -> 'b * 'a) -> 'a -> 'b list * 'a
27 val atleastone : ('a -> 'b * 'a) -> 'a -> 'b list * 'a
33 val everything : ('a, 'b list) parser -> 'a stream -> 'b stream
41 type infixities = {tok : string, prec : int, left_assoc : bool} list
46 val optoks : infixities -> string list
47 val parse_left_infix : string list -> 'a con -> 'a iparser -> 'a iparser
48 val parse_right_infix : string list -> 'a con -> 'a iparser -> 'a iparser
50 val pp_left_infix : string list -> 'a des -> 'a iprinter -> 'a iprinter
51 val pp_right_infix : string list -> 'a des -> 'a iprinter -> 'a iprinter
65 type 'a quotation = 'a frag list
[all...]
H A DmlibResolution.sig28 val new : parameters * units * thm list * thm list -> resolution
34 val deduce : clause -> resolution -> clause list
35 val factor : clause list -> resolution -> clause list * resolution
36 val add : distance * clause list -> resolution -> resolution
H A DmlibSupport.sig19 model_parms : mlibModel.parameters list}
28 val update_model_parms : mlibModel.parameters list parmupdate
35 val new : parameters -> formula list -> clause list -> sos
37 val to_list : sos -> clause list
41 val add : distance * clause list -> sos -> sos
H A DmlibSolver.sig20 type solver = formula list -> thm list option stream
31 val solve : solver -> int -> formula list -> thm list list
32 val find : solver -> formula list -> thm list option
40 thms : thm list, (* Context, assumed consistent *)
41 hyps : thm list} (* Hypothesis, or set of support *)
62 val combine : (cost_fn * solver_node) list
[all...]
H A DmlibUnits.sig17 val addl : thm list -> units -> units
20 val prove : units -> formula list -> thm list option
/seL4-l4v-10.1.1/HOL4/src/Boolify/src/
H A DPreListEncode.sml7 val () = loadPath := ["../../list/src"] @ !loadPath;
39 (Term`encode_prod:('a->bool list)->('b->bool list)-> 'a # 'b -> bool list`,
49 (Term`encode_sum:('a->bool list)->('b->bool list)-> 'a + 'b -> bool list`,
60 (Term`encode_option : ('a -> bool list) -> 'a option -> bool list`,
68 val list_info = Option.valOf (TypeBase.read {Thy = "list", Tyo
[all...]
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/
H A DCOMPILERBODYSIG.sml44 allVal: unit -> (string*values) list,
45 allType: unit -> (string*typeConstrSet) list,
46 allFix: unit -> (string*fixStatus) list,
47 allStruct: unit -> (string*structVals) list,
48 allSig: unit -> (string*signatures) list,
49 allFunct: unit -> (string*functors) list
56 type exportTree = location * ptProperties list
62 nameSpace * (unit->char option) * Universal.universal list ->
64 { fixes: (string * fixStatus) list, values: (string * values) list,
[all...]
/seL4-l4v-10.1.1/HOL4/src/prekernel/
H A DFinalTerm-sig.sml12 val free_vars : term -> term list
13 val free_vars_lr : term -> term list
14 val FVL : term list -> term set -> term set
16 val all_vars : term -> term list
18 val all_atomsl : term list -> term set -> term set
19 val free_varsl : term list -> term list
20 val all_varsl : term list -> term list
21 val type_vars_in_term : term -> hol_type list
[all...]
/seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/
H A DhelperLib.sig21 val RW : thm list -> rule
22 val RW1 : thm list -> rule
30 val quote_to_strings : 'a quotation -> string list
34 val all_distinct : ''a list -> ''a list
36 val collect_term_of_type : hol_type -> term -> term list
37 val find_terml : (term -> bool) -> term -> term list
38 val find_terml_all : (term -> bool) -> term -> term list
43 val list_dest : ('a -> 'a * 'a) -> 'a -> 'a list
44 val list_mk : (term * term -> term) -> term list
[all...]
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/
H A Dtactics.sig31 val print_terms : term list -> unit
33 val print_theorems : thm list -> unit
34 val print_goal : (term list * term) -> unit
100 : thm -> term -> (term * term) list * (hol_type * hol_type) list
102 : thm -> term -> (term * term) list * (hol_type * hol_type) list
106 : thm -> term -> (term * term) list * (hol_type * hol_type) list
108 : thm -> term -> (term * term) list * (hol_typ
[all...]
/seL4-l4v-10.1.1/HOL4/tools/Holmake/
H A DHolmake_types.sig7 type quotation = frag list
10 commands : quotation list }
26 val tokenize : string -> string list
31 type rule_info = {dependencies : string list, commands : string list}
34 (string, {dependencies:string list, commands : quotation list})Binarymap.dict
35 type depdb = (string,string list)Binarymap.dict
38 (ruledb * depdb) -> (ruledb * depdb * string list)
45 a list o
[all...]
/seL4-l4v-10.1.1/HOL4/tools/mlyacc/src/
H A Dsigs.sml36 val text : string list ref
59 NSHIFT of symbol list | POS of string | PURE |
63 datatype rule = RULE of {lhs : symbol, rhs : symbol list,
67 {eop : symbol list,
68 keyword : symbol list,
69 nonterm : (symbol * ty option) list option,
70 prec : (prec * (symbol list)) list,
71 change: (symbol list * symbol list) lis
[all...]
H A Dhdr.sml35 val text = ref (nil: string list)
77 NSHIFT of symbol list | POS of string | PURE |
82 {eop : symbol list,
83 keyword : symbol list,
84 nonterm : (symbol*ty option) list option,
85 prec : (prec * (symbol list)) list,
86 change: (symbol list * symbol list) list,
[all...]
/seL4-l4v-10.1.1/HOL4/src/parse/
H A DOverload.sig7 type overloaded_op_info = {base_type : hol_type, actual_ops : term list,
8 tyavoids : hol_type list}
17 val oinfo_ops : overload_info -> (string * overloaded_op_info) list
20 val print_map : overload_info -> (nthy_rec * string) list
26 (term list -> term list) -> overloaded_op_info ->
32 string -> overload_info -> overload_info * (term list * term list)
35 string -> (nthy_rec list * nthy_rec list)
[all...]
H A DParse_support.sig21 val list_make_comb : locn.locn -> preterm_in_env list -> preterm_in_env
22 val bind_term : locn.locn -> bvar_in_env list ->
24 val make_vstruct : overload_info -> locn.locn -> bvar_in_env list ->
29 (bvar_in_env list * preterm_in_env) list ->
39 val binder_restrictions : unit -> (string * string) list
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/tools/
H A Dtuerk_tacticsLib.sig7 val REWRITE_ASSUMPTIONS_TAC : Abbrev.thm list -> Abbrev.tactic
8 val REWRITE_ALL_TAC : Abbrev.thm list -> Abbrev.tactic
9 val ONCE_REWRITE_ASSUMPTIONS_TAC : Abbrev.thm list -> Abbrev.tactic
10 val ONCE_REWRITE_ALL_TAC : Abbrev.thm list -> Abbrev.tactic
11 val SIMP_ASSUMPTIONS_TAC : simpLib.simpset -> Abbrev.thm list -> Abbrev.tactic
12 val SIMP_ALL_TAC : simpLib.simpset -> Abbrev.thm list -> Abbrev.tactic
25 val SUBGOAL_TAC : Abbrev.term frag list -> Abbrev.tactic
26 val REMAINS_TAC : Abbrev.term frag list -> Abbrev.tactic
28 val SPECL_NO_ASSUM : int -> Abbrev.term list -> Abbrev.tactic
29 val Q_SPEC_NO_ASSUM : int -> Abbrev.term frag list
[all...]
/seL4-l4v-10.1.1/HOL4/src/1/
H A DPmatchHeuristics.sig7 {case_const : term, constructors : term list} option
10 (* given a list of rows of patterns, which column to split on? *)
11 col_fun : thry -> term list list -> int }
23 takes the column-number from the provided list of explicit
24 choices. If the list is too short, the first column is
25 chosen. One should run this heuristic first with an empty list
30 val pheu_manual : int list -> pmatch_heuristic
38 and a list of ranking functions prheuL = [r_1, ... r_j]. The
44 val pheu_rank : (thry -> term list
[all...]
/seL4-l4v-10.1.1/HOL4/src/quotient/src/
H A Dquotient.sig49 val list_cache : unit -> (Type.hol_type * Thm.thm) list
125 Thm.thm -> (* equivalence theorem for element of list *)
126 Thm.thm (* returns equivalence theorem for list:
139 Thm.thm list -> (* base equivalence theorems *)
140 Thm.thm list -> (* polymorphic type operator equivalence theorems *)
183 Thm.thm -> (* quotient theorem for element of list *)
184 Thm.thm (* returns quotient theorem for list:
208 Thm.thm list -> (* quotient theorems for primary lifted types *)
209 Thm.thm list -> (* conditional quotient ths for type operators *)
220 Thm.thm list
[all...]
/seL4-l4v-10.1.1/HOL4/src/quantHeuristics/
H A DquantHeuristicsTools.sig6 val TOP_ONCE_REWRITE_CONV : thm list -> conv;
24 val VARIANT_TAC : term list -> tactic
25 val VARIANT_CONV : term list -> conv
29 val list_variant : term list -> term list -> (term list * (term,term) Lib.subst);
/seL4-l4v-10.1.1/l4v/tools/autocorres/tests/examples/
H A Dheap_wrap.c23 struct list { struct
25 struct list *p;
57 int f8(struct list *l, struct thing *t) {
/seL4-l4v-10.1.1/HOL4/src/TeX/theory_tests/
H A DmdtScript.sml7 val _ = type_abbrev("string", ``:char list``)
16 | Tyapp of type_op => type list type
24 | Defined of num => (string # term) list => term
/seL4-l4v-10.1.1/HOL4/src/bag/
H A DbagLib.sig21 val list_mk_union : term list -> term
29 val list_mk_insert : term list * term -> term
32 val strip_union : term -> term list
50 val mk_bag : term list * hol_type -> term
51 val strip_insert : term -> term list * term
52 val dest_bag : term -> term list * hol_type
59 val SBAG_SOLVE : thm list -> term -> thm
62 val BAG_RESORT_CONV : int list -> conv
64 val GET_BAG_IN_THMS : term -> thm list
68 val get_resort_list___pred : (term -> bool) -> term -> int list
[all...]
/seL4-l4v-10.1.1/HOL4/src/meson/src/
H A DmesonLib.sig20 val GEN_MESON_TAC : int -> int -> int -> thm list -> tactic
21 val MESON_TAC : thm list -> tactic
22 val ASM_MESON_TAC : thm list -> tactic
/seL4-l4v-10.1.1/HOL4/src/patricia/
H A DpatriciaLib.sig19 val add_list : term_ptree -> (num * term) list -> term_ptree
21 val traverse : term_ptree -> num list
22 val keys : term_ptree -> num list
30 val ptree_of_list : (num * term) list -> term_ptree
31 val list_of_ptree : term_ptree -> (num * term) list
32 val ptree_of_nums : num list -> term_ptree
36 val int_add_list : term_ptree -> (int * term) list -> term_ptree
40 val int_ptree_of_list : (int * term) list -> term_ptree
41 val ptree_of_ints : int list -> term_ptree
45 val string_add_list : term_ptree -> (string * term) list
[all...]

Completed in 273 milliseconds

<<11121314151617181920>>