/seL4-l4v-10.1.1/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-10.1.1/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-10.1.1/HOL4/src/tactictoe/src/ |
H A D | tttNumber.sig | 6 val drop_numbering : string list -> string list 7 val replace_at : string list * string list -> string list -> string list
|
H A D | tttPredict.sig | 6 type lbl_t = (string * real * goal * goal list) 7 type fea_t = int list 11 val learn_tfidf : ('a * int list) list -> (int, real) Redblackmap.dict 14 val termknn: int -> goal -> term -> term list 16 (int, real) Redblackmap.dict * ('a * int list) list -> 17 int list -> 'a list 21 (int, real) Redblackmap.dict -> int -> feav_t list [all...] |
/seL4-l4v-10.1.1/HOL4/src/portableML/mosml/concurrent/ |
H A D | Parmap.sig | 3 val parmap : ('a -> 'b) -> 'a list -> 'b list
|
/seL4-l4v-10.1.1/HOL4/src/portableML/poly/concurrent/ |
H A D | Parmap.sig | 4 val parmap : ('a -> 'b) -> 'a list -> 'b list
|
/seL4-l4v-10.1.1/HOL4/src/new-datatype/ |
H A D | Witness.sig | 6 : thm list -> thm option list -> thm list -> thm list
|
/seL4-l4v-10.1.1/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-10.1.1/l4v/tools/autocorres/tests/examples/ |
H A D | list_rev.c | 18 struct node *reverse(struct node *list) { argument 20 while (list) { 21 struct node *next = list->next; 22 list->next = rev; rev = list; list = next;
|
H A D | list.c | 16 struct node *insert(struct node *x, struct node *list) { argument 17 x->next = list; 21 struct node *sorted_insert(struct node *x, struct node *list) { argument 22 struct node *prev = 0, *cur = list; 28 return list; 30 x->next = list; 39 return list; 42 struct node *reverse(struct node *list) { argument 44 while (list) { 45 struct node *next = list 53 revappend(struct node *list, struct node *dest) argument [all...] |
/seL4-l4v-10.1.1/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-10.1.1/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-10.1.1/HOL4/src/parse/ |
H A D | PrecAnalysis.sig | 5 type rell_transform = rel list -> rel list 8 (string * bool * string) list 17 (string * string -> 'a option) -> rel list -> 18 (string * string * 'a) list 19 val remove_listrels : (string * string * mlsp) list -> rel list -> 20 rel list * (mlsp * int list) list [all...] |
/seL4-l4v-10.1.1/HOL4/src/prekernel/ |
H A D | Lib.sig | 8 type ('a, 'b) subst = {redex: 'a, residue: 'b} list 18 val U : ''a list list -> ''a list 25 val all2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool 26 val all : ('a -> bool) -> 'a list -> bool 28 val append : 'a list -> 'a list -> 'a list [all...] |
/seL4-l4v-10.1.1/l4v/tools/c-parser/testfiles/ |
H A D | struct_ptr_fn.c | 11 struct list { struct 13 struct list *next; 16 int last(struct list *nodeptr)
|
/seL4-l4v-10.1.1/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-10.1.1/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-10.1.1/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-10.1.1/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...] |
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
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-10.1.1/HOL4/polyml/basis/ |
H A D | ListSignature.sml | 23 datatype list = datatype list type 24 (* G&R include the definition of list below in their "Interface". This is illegal. *) 25 (*datatype 'a list = nil | :: of 'a * 'a list *) 27 val null : 'a list -> bool 28 val length : 'a list -> int 29 val @ : ('a list * 'a list) -> 'a list [all...] |
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
H A D | functionEncodeLib.sig | 19 val resolve_head_term : bool -> thm -> thm -> term list -> term list * thm 27 val partial_resolve : bool -> (term -> thm) list -> thm -> thm 28 val full_resolve : (term -> thm) list -> thm -> thm 29 val resolve_functions : thm list -> (term -> thm) list 31 thm list -> thm list * thm list -> thm list * th [all...] |