/seL4-l4v-master/HOL4/src/simp/src/ |
H A D | Cache.sig | 23 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 D | HM_Cline.sig | 9 val option_descriptions : t HM_Core_Cline.cline_result GetOpt.opt_descr list
|
/seL4-l4v-master/HOL4/examples/ARM/v4/ |
H A D | arm_evalLib.sig | 14 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 D | CCSSyntax.sig | 49 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 D | translateLib.sig | 5 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 D | Options.sig | 13 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 D | Parse.sig | 38 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 D | Tptp.sig | 18 {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 D | boolTools.sig | 23 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 D | file_readerLib.sig | 12 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 D | x64_Lib.sig | 8 val x64_test : string -> (string * string * string) list -> unit
|
/seL4-l4v-master/HOL4/examples/miller/formalize/ |
H A D | extra_pred_setTools.sig | 9 val PSET_TAC : Thm.thm list -> Abbrev.tactic
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Options.sig | 13 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 D | Parse.sig | 38 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 D | Tptp.sig | 18 {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 D | BuildCommand.sig | 8 {extra_impl_deps : dep list,
|
/seL4-l4v-master/HOL4/src/1/ |
H A D | thmpos_dtype.sml | 8 | Pos of (Term.term list -> Term.term)
|
H A D | Drule.sig | 10 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 D | mleDiophProve.sig | 10 val DIOPH_PROVE : term * int list -> thm
|
/seL4-l4v-master/HOL4/src/AI/proof_search/ |
H A D | psMCTS.sig | 15 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 D | hhTranslate.sig | 9 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 D | mlTacticData.sig | 9 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 D | buildcline.sig | 10 val cline_opt_descrs : t cline_result GetOpt.opt_descr list
|
/seL4-l4v-master/HOL4/src/boss/theory_tests/ |
H A D | caseEqAbbrevScript.sml | 5 Type foo = ���:'a list���
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | List.sml | 23 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...] |