Searched refs:list (Results 301 - 325 of 2047) sorted by relevance

<<11121314151617181920>>

/seL4-l4v-master/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-master/HOL4/tools/Holmake/mosml/
H A DHM_Cline.sig9 val option_descriptions : t HM_Core_Cline.cline_result GetOpt.opt_descr list
/seL4-l4v-master/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-master/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-master/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
/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DOptions.sig13 type proc = string * string list -> unit
22 {switches : string list, arguments : string list,
47 val enumOpt : string list -> (string,'x) mkProc
55 val basicOptions : opt list
63 footer : string, options : opt list}
91 val processOptions : allOptions -> string list -> string list * string list
H A DParse.sig38 val first : ('a -> 'b * 'a) list -> 'a -> 'b * 'a
42 val many : ('a -> 'b * 'a) -> 'a -> 'b list * 'a
44 val atLeastOne : ('a -> 'b * 'a) -> 'a -> 'b list * 'a
70 val fromList : ('a,'b) parser -> 'a list -> 'b
72 val everything : ('a, 'b list) parser -> 'a Stream.stream -> 'b Stream.stream
80 {chars : char list Stream.stream,
85 val exactCharList : char list -> (char,unit) parser
89 val escapeString : {escape : char list} -> (char,string) parser
110 type 'a quotation = 'a frag list
H A DTptp.sig18 {functionMapping : {name : Name.name, arity : int, tptp : string} list,
19 relationMapping : {name : Name.name, arity : int, tptp : string} list} ->
102 CnfFormulaBody of literal list
113 parents : formulaName list}
116 parents : formulaName list}
119 parents : formulaName list}
146 val freeVarsListFormula : formula list -> NameSet.set
157 CnfClauseSource of formulaName * literal list
178 type comments = string list
180 type includes = string list
[all...]
/seL4-l4v-master/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-master/HOL4/examples/machine-code/graph/
H A Dfile_readerLib.sig12 val read_files : string -> string list -> unit
13 val section_body : string -> (int * string * string) list
14 val section_io : string -> int list * int * bool
16 val section_names : unit -> string list
/seL4-l4v-master/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-master/HOL4/examples/miller/formalize/
H A Dextra_pred_setTools.sig9 val PSET_TAC : Thm.thm list -> Abbrev.tactic
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DOptions.sig13 type proc = string * string list -> unit
22 {switches : string list, arguments : string list,
47 val enumOpt : string list -> (string,'x) mkProc
55 val basicOptions : opt list
63 footer : string, options : opt list}
91 val processOptions : allOptions -> string list -> string list * string list
H A DParse.sig38 val first : ('a -> 'b * 'a) list -> 'a -> 'b * 'a
42 val many : ('a -> 'b * 'a) -> 'a -> 'b list * 'a
44 val atLeastOne : ('a -> 'b * 'a) -> 'a -> 'b list * 'a
70 val fromList : ('a,'b) parser -> 'a list -> 'b
72 val everything : ('a, 'b list) parser -> 'a Stream.stream -> 'b Stream.stream
80 {chars : char list Stream.stream,
85 val exactCharList : char list -> (char,unit) parser
89 val escapeString : {escape : char list} -> (char,string) parser
110 type 'a quotation = 'a frag list
H A DTptp.sig18 {functionMapping : {name : Name.name, arity : int, tptp : string} list,
19 relationMapping : {name : Name.name, arity : int, tptp : string} list} ->
102 CnfFormulaBody of literal list
113 parents : formulaName list}
116 parents : formulaName list}
119 parents : formulaName list}
146 val freeVarsListFormula : formula list -> NameSet.set
157 CnfClauseSource of formulaName * literal list
178 type comments = string list
180 type includes = string list
[all...]
/seL4-l4v-master/HOL4/tools/Holmake/
H A DBuildCommand.sig8 {extra_impl_deps : dep list,
/seL4-l4v-master/HOL4/src/1/
H A Dthmpos_dtype.sml8 | Pos of (Term.term list -> Term.term)
H A DDrule.sig10 val LIST_MK_EXISTS : term list -> thm -> thm
13 val EXISTS_LEFT : term list -> thm -> thm
17 -> thm list -> thm -> thm
27 val SPECL : term list -> thm -> thm
36 val SUBS : thm list -> thm -> thm
37 val SUBS_OCCS : (int list * thm) list -> thm -> thm
45 val CONJ_DISCHL : term list -> thm -> thm
51 val ISPECL : term list -> thm -> thm
57 val REORDER_ANTS_MOD : (term list
[all...]
/seL4-l4v-master/HOL4/examples/AI_tasks/
H A DmleDiophProve.sig10 val DIOPH_PROVE : term * int list -> thm
/seL4-l4v-master/HOL4/src/AI/proof_search/
H A DpsMCTS.sig15 type id = int list
17 type 'b pol = (('b * real) * id) list
26 val gamma_distrib : real -> (real * real) list
34 available_movel : 'a -> 'b list,
39 movel : 'b list
42 type ('a,'b) player = 'a -> real * ('b * real) list
72 val mostexplored_path : ('a,'b) tree -> id -> id list
74 val trace_win : ('a,'b) tree -> id -> ('a,'b) node list
75 val trace_win_movel : ('a,'b) tree -> id -> ('a * 'b) list
/seL4-l4v-master/HOL4/src/holyhammer/
H A DhhTranslate.sig9 val atoms : term -> term list
15 val RPT_LIFT_CONV : int ref -> term -> thm list
31 val strip_type : hol_type -> (hol_type list * hol_type)
32 val collect_arity_noapp : term -> (term * int) list
/seL4-l4v-master/HOL4/src/AI/machine_learning/
H A DmlTacticData.sig9 type call = {stac : stac, ogl : int list, fea : mlFeature.fea}
21 val export_calls : string -> (loc * call) list -> unit
22 val import_calls : string -> (loc * call) list
23 val import_tacdata : string list -> tacdata
/seL4-l4v-master/HOL4/tools/
H A Dbuildcline.sig10 val cline_opt_descrs : t cline_result GetOpt.opt_descr list
/seL4-l4v-master/HOL4/src/boss/theory_tests/
H A DcaseEqAbbrevScript.sml5 Type foo = ���:'a list���
/seL4-l4v-master/HOL4/polyml/basis/
H A DList.sml23 datatype list = datatype list type
37 list if the second list is empty. *)
64 (* TODO: Many of these functions involve recursing down the list and
65 so require stack space proportional to the length of the list.
68 of constructing the list twice. *)
107 implementation? e.g. recurse down the list and then reverse it. *)
150 val null : 'a list -> bool = List.null
151 val hd : 'a list
[all...]

Completed in 145 milliseconds

<<11121314151617181920>>