/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | folMapping.sig | 16 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 D | mlibParser.sig | 26 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 D | mlibResolution.sig | 28 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 D | mlibSupport.sig | 19 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 D | mlibSolver.sig | 20 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 D | mlibUnits.sig | 17 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 D | PreListEncode.sml | 7 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 D | COMPILERBODYSIG.sml | 44 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 D | FinalTerm-sig.sml | 12 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 D | helperLib.sig | 21 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 D | tactics.sig | 31 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 D | Holmake_types.sig | 7 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 D | sigs.sml | 36 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 D | hdr.sml | 35 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 D | Overload.sig | 7 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 D | Parse_support.sig | 21 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 D | tuerk_tacticsLib.sig | 7 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 D | PmatchHeuristics.sig | 7 {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 D | quotient.sig | 49 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 D | quantHeuristicsTools.sig | 6 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 D | heap_wrap.c | 23 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 D | mdtScript.sml | 7 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 D | bagLib.sig | 21 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 D | mesonLib.sig | 20 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 D | patriciaLib.sig | 19 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...] |