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

<<11121314151617181920>>

/seL4-l4v-10.1.1/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-10.1.1/HOL4/src/portableML/monads/
H A Derrormonad.sig21 val mmap : ('a -> ('b, 'c, 'd) t) -> 'a list -> ('b, 'c list, 'd) t
22 val foldlM : ('e * 'acc -> ('s,'acc,'error)t) -> 'acc -> 'e list ->
/seL4-l4v-10.1.1/HOL4/tools/Holmake/
H A DHolmake_tools_dtype.sml23 datatype buildcmds = Compile of File list
24 | BuildScript of string * File list
25 | BuildArticle of string * File list
/seL4-l4v-10.1.1/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-10.1.1/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-10.1.1/HOL4/examples/formal-languages/regular/
H A DRegexp_Type.sig11 | Or of regexp list
15 val alphabet : char list
21 val charset_of : char list -> charset
22 val charset_elts : charset -> char list
56 = Ap of string * tree list
63 | Pack of packelt list
65 val tree_parse : substring -> tree list * substring
67 val quote_to_tree : 'a frag list -> tree
73 val fromQuote : 'a frag list -> regexp
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/step/
H A Darm_configLib.sig6 val mk_config_terms: string -> term list
/seL4-l4v-10.1.1/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
H A DTactical.sig16 val THENL : ('a,'b) gentactic * tactic list -> ('a,'b) gentactic
17 val >| : ('a,'b) gentactic * tactic list -> ('a,'b) gentactic
19 val THENL : tactic * tactic list -> tactic
20 val THENL : list_tactic * tactic list -> list_tactic
34 val TACS_TO_LT : tactic list -> list_tactic
64 val ADD_SGS_TAC : term list -> tactic -> tactic
65 val EVERY : tactic list -> tactic
66 val EVERY_LT : list_tactic list -> list_tactic
67 val FIRST : tactic list -> tactic
68 val MAP_EVERY : ('a -> tactic) -> 'a list
[all...]
/seL4-l4v-10.1.1/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-10.1.1/HOL4/src/datatype/mutrec/
H A DConsThms.sig12 argument_extraction_definitions : (string * thm) list}
/seL4-l4v-10.1.1/HOL4/src/metis/
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-10.1.1/HOL4/src/parse/
H A DFCNet.sig8 val match : term -> 'a t -> 'a list
H A DPretype_dtype.sml6 | Tyop of {Thy:string,Tyop:string, Args: pretype list}
H A Dterm_tokens.sig12 val lex : string list -> 'a qbuf.qbuf -> 'a term_token locn.located option
16 val user_split_ident : string list -> string -> (string * string)
25 val lextest : string list -> string -> 'a term_token list
/seL4-l4v-10.1.1/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-10.1.1/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 *)
/seL4-l4v-10.1.1/HOL4/src/simp/src/
H A DCache.sig23 list of those terms within it that will be treated as variables.
38 val CACHE :(term -> bool) * (thm list->conv) -> (thm list -> conv) * cache
40 val cache_values : cache -> (term * (term list * thm option) list) list
41 val RCACHE : (term -> term list) * (term -> bool) * (thm list -> conv) ->
42 (thm list -> conv) * cache
/seL4-l4v-10.1.1/HOL4/tools/Holmake/mosml/
H A DHM_Cline.sig10 val option_descriptions : t HM_Core_Cline.cline_result GetOpt.opt_descr list
/seL4-l4v-10.1.1/HOL4/examples/machine-code/garbage-collectors/
H A DboolTools.sig23 val ORELSE_STRENGTHEN_CONV : conv list -> conv;
24 val CONJ_ASSUMPTIONS_STRENGTHEN_CONV : conv -> term list -> conv;
35 val COND_REWRITE_CONV : thm list -> term -> thm
36 val GUARDED_COND_REWRITE_CONV : (term -> bool) -> thm list -> term -> thm
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/
H A Dx64_Lib.sig8 val x64_test : string -> (string * string * string) list -> unit
/seL4-l4v-10.1.1/HOL4/examples/miller/formalize/
H A Dextra_pred_setTools.sig9 val PSET_TAC : Thm.thm list -> Abbrev.tactic
/seL4-l4v-10.1.1/HOL4/examples/ARM/v4/
H A Darm_evalLib.sig14 val hol_assemble1 : term -> Arbnum.num -> term frag list -> term
15 val hol_assemble : term -> Arbnum.num -> term frag list list -> term
16 val list_assemble : term -> string list -> term
24 val set_registers : term -> term frag list -> term
25 val set_status_registers : term -> term frag list -> term
32 val print_regs : (int * mode) list -> term -> unit
42 val eval_cp : int * term * term * term * term * term -> thm list
45 val eval : int * term * term * term -> thm list
/seL4-l4v-10.1.1/HOL4/examples/CCS/
H A DCCSSyntax.sig49 val flat_sum : term -> term list
50 val ladd : term -> term list -> term list
51 val FIND_SMD : term list -> term -> term list -> term -> term list * term list
52 val build_sum : term list -> term
53 val sum_to_fun : term list -> term -> term -> term
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/
H A DtranslateLib.sig5 val CHOOSEP_TAC : thm list -> tactic
6 val CHOOSEP : thm list -> term -> thm
17 val strip_cons : term -> term list
24 val DISJ_CASES_UNIONL : thm -> thm list -> thm

Completed in 146 milliseconds

<<11121314151617181920>>