/seL4-l4v-master/HOL4/examples/l3-machine-code/lib/ |
H A D | Set.sig | 7 val diff : ''a list * ''a list -> ''a list 8 val equal : ''a list * ''a list -> bool 9 val insert : ''a * ''a list -> ''a list 10 val intersect : ''a list * ''a list -> ''a list [all...] |
/seL4-l4v-master/HOL4/src/portableML/ |
H A D | AList.sig | 10 val lookup: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option 11 val defined: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool 13 -> ('a * 'b) list -> ('a * 'b) list 15 -> ('a * 'b) list -> ('a * 'b) list 17 -> ('b * 'c) list -> ('b * 'c) list 19 -> ('b * 'c) list -> ('b * 'c) list [all...] |
/seL4-l4v-master/HOL4/src/portableML/mosml/concurrent/ |
H A D | Parmap.sig | 3 val parmap : ('a -> 'b) -> 'a list -> 'b list
|
/seL4-l4v-master/HOL4/src/portableML/poly/concurrent/ |
H A D | Parmap.sig | 4 val parmap : ('a -> 'b) -> 'a list -> 'b list
|
/seL4-l4v-master/HOL4/src/new-datatype/ |
H A D | Witness.sig | 6 : thm list -> thm option list -> thm list -> thm list
|
/seL4-l4v-master/HOL4/examples/formal-languages/regular/ |
H A D | regexpMisc.sig | 9 val spread : 'a -> 'a list -> 'a list 12 -> 'a list -> string list 15 val bigUpto : IntInf.int -> IntInf.int -> IntInf.int list 16 val bigIntervals : IntInf.int list -> (IntInf.int * IntInf.int) list 17 val intervals : int list -> (int * int) list 22 val cross : 'a list [all...] |
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Sharing.sig | 21 val map : ('a -> 'a) -> 'a list -> 'a list 23 val revMap : ('a -> 'a) -> 'a list -> 'a list 25 val maps : ('a -> 's -> 'a * 's) -> 'a list -> 's -> 'a list * 's 27 val revMaps : ('a -> 's -> 'a * 's) -> 'a list -> 's -> 'a list * 's 29 val updateNth : int * 'a -> 'a list -> 'a list [all...] |
H A D | Useful.sig | 87 val listEqual : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool 100 val lexCompare : ('a * 'a -> order) -> 'a list * 'a list -> order 110 val cons : 'a -> 'a list -> 'a list 112 val hdTl : 'a list -> 'a * 'a list 114 val append : 'a list -> 'a list [all...] |
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Sharing.sig | 21 val map : ('a -> 'a) -> 'a list -> 'a list 23 val revMap : ('a -> 'a) -> 'a list -> 'a list 25 val maps : ('a -> 's -> 'a * 's) -> 'a list -> 's -> 'a list * 's 27 val revMaps : ('a -> 's -> 'a * 's) -> 'a list -> 's -> 'a list * 's 29 val updateNth : int * 'a -> 'a list -> 'a list [all...] |
H A D | Useful.sig | 87 val listEqual : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool 100 val lexCompare : ('a * 'a -> order) -> 'a list * 'a list -> order 110 val cons : 'a -> 'a list -> 'a list 112 val hdTl : 'a list -> 'a * 'a list 114 val append : 'a list -> 'a list [all...] |
/seL4-l4v-master/l4v/tools/autocorres/tests/examples/ |
H A D | list_rev.c | 14 struct node *reverse(struct node *list) argument 17 while (list) { 18 struct node *next = list->next; 19 list->next = rev; 20 rev = list; 21 list = next;
|
H A D | list.c | 12 struct node *insert(struct node *x, struct node *list) argument 14 x->next = list; 18 struct node *sorted_insert(struct node *x, struct node *list) argument 20 struct node *prev = 0, *cur = list; 26 return list; 28 x->next = list; 37 return list; 40 struct node *reverse(struct node *list) argument 43 while (list) { 44 struct node *next = list 52 revappend(struct node *list, struct node *dest) argument [all...] |
/seL4-l4v-master/HOL4/src/AI/sml_inspection/ |
H A D | smlPrettify.sig | 6 val elim_par : string list -> string list 7 val elim_infix : string list -> string list 8 val elim_struct : string list -> string list 9 val elim_dbfetch : string list -> string list 11 val requote : string list -> string list [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw2/ |
H A D | compiler.sig | 5 val f_compile : thm list -> ((thm * thm) list, thm list * thm list) Lib.verdict 6 (* val b_compile : ((thm * thm) list, 'c) Lib.verdict -> ((thm * thm) list, 'c) Lib.verdict 7 val pp_compile : thm list -> ((thm * thm) list, thm list * thm list) Li [all...] |
/seL4-l4v-master/HOL4/src/prekernel/ |
H A D | Lib.sig | 9 type ('a, 'b) subst = {redex: 'a, residue: 'b} list 20 val U : ''a list list -> ''a list 27 val all2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool 28 val all : ('a -> bool) -> 'a list -> bool 30 val append : 'a list -> 'a list -> 'a list [all...] |
/seL4-l4v-master/HOL4/src/AI/ |
H A D | aiLib.sig | 7 val number_fst : int -> 'a list -> (int * 'a) list 8 val number_snd : int -> 'a list -> ('a * int) list 10 val vector_to_list : 'a vector -> 'a list 31 val list_rmax : real list -> real 32 val list_imax : int list -> int 33 val list_imin : int list -> int 35 val all_subterms : term -> term list 36 val div_equal : int -> int -> int list [all...] |
/seL4-l4v-master/HOL4/src/AI/proof_search/ |
H A D | psTermGen.sig | 6 val nterm : term list -> int * hol_type -> real 7 val random_term : term list -> int * hol_type -> term 8 val random_terml : term list -> int * hol_type -> int -> term list 9 val gen_term : term list -> int * hol_type -> term list
|
/seL4-l4v-master/l4v/tools/c-parser/testfiles/ |
H A D | struct_ptr_fn.c | 7 struct list { struct 9 struct list *next; 12 int last(struct list *nodeptr)
|
/seL4-l4v-master/HOL4/examples/machine-code/graph/ |
H A D | backgroundLib.sig | 6 val try_map : ('a -> 'b) -> 'a list -> 'b list 7 val append_lists : 'a list list -> 'a list 8 val diff : ''a list -> ''a list -> ''a list 9 val drop : int -> 'a list -> 'a list [all...] |
H A D | graph_specsLib.sig | 5 val derive_insts_for : string -> Thm.thm list 6 val print_graph_spec_report : unit -> unit list 7 val try_map : ('a -> 'b) -> ('a -> 'c) -> 'a list -> 'c list
|
/seL4-l4v-master/HOL4/src/num/arith/src/ |
H A D | Sol_ranges.sig | 5 val Shostak : (int * (string * int) list) list -> (string * int) list
|
H A D | Sup_Inf.sig | 5 datatype bound = Bound of Rationals.rat * (string * Rationals.rat) list 6 | Max_bound of bound list 7 | Min_bound of bound list 12 val SUP : (int * (string * int) list) list -> 13 (bound * (string list)) -> 15 val INF : (int * (string * int) list) list -> 16 (bound * (string list)) -> 20 (int * (string * int) list) lis [all...] |
/seL4-l4v-master/HOL4/examples/countable/ |
H A D | countableLib.sig | 3 val mk_count_aux_inj_rwt_ttac : hol_type list -> tactic option -> thm list 4 val mk_count_aux_inj_rwt : hol_type list -> thm list
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm8/prog/ |
H A D | arm8_progLib.sig | 4 val arm8_spec: string -> Thm.thm list 5 val arm8_spec_code: string quotation -> Thm.thm list list 6 val arm8_spec_hex: string -> Thm.thm list
|
/seL4-l4v-master/HOL4/src/1/ |
H A D | Ho_Rewrite.sig | 5 val mk_rewrites : thm -> thm list 7 val implicit_rewrites : unit -> thm list 8 val set_implicit_rewrites : thm list -> unit 9 val add_implicit_rewrites : thm list -> unit 11 val GEN_REWRITE_CONV : (conv -> conv) -> thm list -> conv 12 val GEN_REWRITE_RULE : (conv -> conv) -> thm list -> thm -> thm 13 val GEN_REWRITE_TAC : (conv -> conv) -> thm list -> tactic 15 val PURE_REWRITE_CONV : thm list -> conv 16 val REWRITE_CONV : thm list -> conv 17 val HIGHER_REWRITE_CONV : thm list [all...] |