Searched refs:list (Results 276 - 300 of 2047) sorted by relevance

<<11121314151617181920>>

/seL4-l4v-master/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-master/l4v/tools/autocorres/tests/examples/
H A Dheap_wrap.c19 struct list { struct
21 struct list *p;
60 int f8(struct list *l, struct thing *t)
/seL4-l4v-master/HOL4/src/IndDef/
H A DIndDefLib.sig6 val term_of : term quotation -> term * locn.locn list
7 val term_of_absyn : Absyn.absyn -> term * locn.locn list
14 (term * locn.locn list) -> thm * thm * thm
22 val thy_monos : string -> thm list
24 type rule_induction_map = ({Thy:string,Name:string},thm list) Binarymap.dict
25 val thy_rule_inductions : string -> thm list
/seL4-l4v-master/HOL4/examples/formal-languages/regular/
H A DRegexp_Type.sig8 val alphabet : char list
14 val charset_of : char list -> charset
15 val charset_elts : charset -> char list
28 | Or of regexp list
50 val catlist : regexp list -> regexp
51 val strip_cat : regexp -> regexp list
52 val dots : int -> regexp list
53 val mk_or : regexp list -> regexp
57 = Ap of string * tree list
65 val tree_parse : substring -> tree list * substrin
[all...]
/seL4-l4v-master/HOL4/src/TeX/theory_tests/
H A DmdtScript.sml7 val _ = type_abbrev_pp("string", ``:char list``)
16 | Tyapp of type_op => type list type
24 | Defined of num => (string # term) list => term
/seL4-l4v-master/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-master/HOL4/src/finite_maps/
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...]
/seL4-l4v-master/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-master/HOL4/src/metis/
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
H A DmlibKernel.sig18 val dest_thm : thm -> formula list * (inference * thm list)
21 val AXIOM : formula list -> thm
27 val EQUALITY : formula -> int list -> term -> bool -> thm -> thm
/seL4-l4v-master/HOL4/src/portableML/
H A DProfile.sig14 val results : unit -> (string * call_info) list
17 val print_profile_results : (string * call_info) list -> unit
20 val output_profile_results : TextIO.outstream -> (string * call_info) list ->
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/extract/
H A Dlisp_extractLib.sig9 val pure_extract_mutual_rec : string list -> tactic option -> thm
15 val deep_embeddings : string -> (thm * thm) list -> thm * thm list
/seL4-l4v-master/HOL4/tools/Holmake/
H A DHolmake_tools_dtype.sml23 Compile of 'dep list * 'extra
24 | BuildScript of string * 'dep list * 'extra
25 | BuildArticle of string * 'dep list * 'extra
/seL4-l4v-master/HOL4/src/AI/proof_search/
H A DpsBigSteps.sig12 type 'a rlex = ('a * real list) list
29 val run_bigsteps : ('a,'b) bsobj -> 'a -> bool * 'a rlex * ('a,'b) node list
/seL4-l4v-master/HOL4/src/portableML/monads/
H A Derrormonad.sig22 val mmap : ('a -> ('b, 'c, 'd) t) -> 'a list -> ('b, 'c list, 'd) t
23 val foldlM : ('e * 'acc -> ('s,'acc,'error)t) -> 'acc -> 'e list ->
/seL4-l4v-master/HOL4/examples/elliptic/c_output/
H A Dc_outputLib.sig15 the function main_func. The parameter tests is a list of pairs
16 (f, (arg, res) list). f is the function to be tested, the other list
20 val translate_to_c : string -> string -> thm list -> thm list -> term -> (term * (term * term) list) list -> unit;
24 It generates a random list of word32-pairs with pair_size elements in
29 val generate_word_pair_list : int -> int -> int -> term list
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/step/
H A Darm_configLib.sig6 val mk_config_terms: string -> term list
/seL4-l4v-master/HOL4/src/1/
H A DPrim_rec.sig13 val doms_of_tyaxiom : thm -> hol_type list
20 val type_constructors : thm -> string -> term list
21 val type_constructors_with_args : thm -> string -> term list
31 val define_case_constant : thm -> thm list
40 Similarly, this function returns a list of theorems where each theorem
41 in the list is the cases theorem for a type characterised in the axiom.
44 val prove_cases_thm : thm -> thm list
46 val prove_constructors_distinct : thm -> thm option list
47 val prove_constructors_one_one : thm -> thm option list
/seL4-l4v-master/HOL4/src/TeX/
H A DEmitTeX.sig9 val non_type_definitions : string -> (string * thm) list
10 val non_type_theorems : string -> (string * thm) list
11 val datatype_theorems : string -> (string * thm) list
29 val print_theories_as_tex_doc : string list -> string -> unit
/seL4-l4v-master/HOL4/src/datatype/mutrec/
H A DConsThms.sig12 argument_extraction_definitions : (string * thm) list}
/seL4-l4v-master/HOL4/src/parse/
H A DPretype_dtype.sml6 | Tyop of {Thy:string,Tyop:string, Args: pretype list}
H A Dterm_tokens.sig13 val lex : string list -> 'a qbuf.qbuf -> 'a term_token locn.located option
17 val user_split_ident : string list -> string -> (string * string)
24 val lextest : string list -> string -> 'a term_token list
/seL4-l4v-master/HOL4/src/portableML/poly/
H A DPar_Exn.sml10 val make: exn list -> exn
11 val dest: exn -> exn list option
12 val is_interrupted: 'a Exn.result list -> bool
13 val release_all: 'a Exn.result list -> 'a list
14 val release_first: 'a Exn.result list -> 'a list
22 exception Par_Exn of exn list;
23 (*non-empty list with unique identified elements sorted by exn_ord;
/seL4-l4v-master/HOL4/src/quotient/examples/
H A Dind_rel.sig9 Term.term list -> (* patterns *)
11 Term.term list (* each term corresponds to a quantified rule *)
13 Term.term list -> (* patterns *)
19 Thm.thm list (* inversion theorems *)

Completed in 195 milliseconds

<<11121314151617181920>>