/seL4-l4v-master/HOL4/src/simp/src/ |
H A D | Unify.sml | 33 fun bind env v t = if occ env v t then failwith "occurs" else function
|
/seL4-l4v-master/HOL4/src/portableML/monads/ |
H A D | errormonad.sig | 12 val bind : ('a, 'b, 'c) t * ('b -> ('a, 'd, 'c) t) -> ('a, 'd, 'c) t value
|
H A D | errormonad.sml | 16 fun bind (m1,f) env0 = function
|
/seL4-l4v-master/HOL4/src/num/arith/src/ |
H A D | Sup_Inf.sml | 137 and bind = sum_bindings (tl bind1) (tl bind2) value [all...] |
/seL4-l4v-master/HOL4/src/portableML/ |
H A D | seq.sig | 32 val bind : 'a seq -> ('a -> 'b seq) -> 'b seq value
|
H A D | seq.sml | 81 fun bind LNIL f = LNIL function
|
/seL4-l4v-master/HOL4/examples/acl2/tests/inputs/ |
H A D | problem-set-1-answers.lisp | 591 (defun bind (var val alist) function
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | Pretype.sml | 71 fun bind i pty : unit in_env = function
|
/seL4-l4v-master/HOL4/src/postkernel/ |
H A D | ThyDataSexp.sml | 347 fun bind NONE f = NONE function
|
/seL4-l4v-master/HOL4/src/coretypes/ |
H A D | pairTools.sml | 276 val bind = mk_eq(vstr', arg) value
|
/seL4-l4v-master/HOL4/src/monad/ |
H A D | monadsyntax.sml | 407 val {bind,ignorebind,unit,fail,choice,guard} = getMI fname s value 420 val {bind,ignorebin value [all...] |
/seL4-l4v-master/HOL4/examples/elliptic/ |
H A D | Useful.sig | 113 val bind : ('s -> 'a * 's) -> ('a -> 's -> 'b * 's) -> 's -> 'b * 's value
|
H A D | Useful.sml | 191 fun bind f (g : 'a -> 's -> 'b * 's) = uncurry g o f; function
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibTerm.sml | 346 fun bind s (v,t) = Fn (s, [Var v, t]) function
|
H A D | mlibUseful.sig | 53 val bind : ('s -> 'a * 's) -> ('a -> 's -> 'b * 's) -> 's -> 'b * 's value
|
H A D | mlibUseful.sml | 147 fun bind f (g : 'a -> 's -> 'b * 's) = uncurry g o f; function
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Term.sml | 675 fun bind (v,t) = function
|
H A D | Useful.sig | 71 val bind : ('s -> 'a * 's) -> ('a -> 's -> 'b * 's) -> 's -> 'b * 's value
|
H A D | Useful.sml | 119 fun bind f (g : 'a -> 's -> 'b * 's) = uncurry g o f; function
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Term.sml | 675 fun bind (v,t) = function
|
H A D | Useful.sig | 71 val bind : ('s -> 'a * 's) -> ('a -> 's -> 'b * 's) -> 's -> 'b * 's value
|
H A D | Useful.sml | 119 fun bind f (g : 'a -> 's -> 'b * 's) = uncurry g o f; function
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | Socket.sml | 78 val bind : ('af, 'sock_type) sock * 'af sock_addr -> unit value 429 fun bind (SOCK s, SOCKADDR a) = doBindCall(s, a) function
|
/seL4-l4v-master/HOL4/src/num/termination/ |
H A D | TotalDefn.sml | 635 val bind = stem ^ !Defn.def_suffix value
|
/seL4-l4v-master/HOL4/src/0/ |
H A D | Term.sml | 665 fun bind (v as Fv _) vmap k = k (lookup v vmap) function 682 let fun bind (v as Fv _) i = if v=Bvar then Bv i else v function [all...] |