| /seL4-l4v-master/HOL4/src/1/theory_tests/ |
| H A D | gh168dScript.sml | 9 val ty1 = ``:gh294a$foo`` value
|
| /seL4-l4v-master/HOL4/src/monad/more_monads/ |
| H A D | state_transformerSyntax.sml | 23 val (ty1, ty2) = Lib.with_exn Type.dom_rng ty err value
52 val (ty1, ty2) = dest_monad_type (Term.type_of tm2) value
|
| /seL4-l4v-master/HOL4/src/n-bit/ |
| H A D | selftest.sml | 43 val ty1 = listSyntax.mk_list_type (wordsSyntax.mk_int_word_type 32) value
49 val ty1 = fcpSyntax.mk_cart_type value
|
| /seL4-l4v-master/HOL4/src/combin/ |
| H A D | combinSyntax.sml | 26 val (ty1,ty2) = dom_rng frng value
35 val (ty1,ty2) = dom_rng frng value
42 let val (ty1,rng) = dom_rng (type_of f) value
|
| /seL4-l4v-master/HOL4/src/coretypes/ |
| H A D | PairedLambda.sml | 255 val (ty1, ty2) = Type.dom_rng (Term.type_of func) value
|
| H A D | pairSyntax.sml | 49 val ty1 = type_of fst value
101 val (ty1, ty2) = dest_prod (type_of tm) value
109 val (ty1, ty2) = dest_prod (type_of tm) value
[all...] |
| /seL4-l4v-master/HOL4/src/parse/ |
| H A D | parse_type.sml | 181 val ty1 = prse fb value
246 val ty1 = let value
276 val ty1 = next_level strm value
283 val ty1 = next_level strm value
292 val ty1 value
[all...] |
| H A D | Literal.sml | 42 let val (ty1,ty2) = Type.dom_rng ty value
|
| H A D | Overload.sml | 488 val ty1 = #base_type op1 value
[all...] |
| /seL4-l4v-master/HOL4/src/pred_set/src/ |
| H A D | PGspec.sml | 50 val (ty1,ty2) = (case alist of [a,b] => (a,b) value
|
| /seL4-l4v-master/HOL4/examples/miller/ho_prover/ |
| H A D | unifyTools.sml | [all...] |
| H A D | skiTools.sml | 99 val (ty1, ty2) = Df type_of (tm1, tm2) value
|
| /seL4-l4v-master/HOL4/src/tactictoe/src/ |
| H A D | tttTrain.sml | 67 val ty1 = type_of v value
|
| /seL4-l4v-master/HOL4/src/experimental-kernel/ |
| H A D | Type.sml | 154 fun (ty1 --> ty2) = Tyapp(funref, [ty1, ty2]) function
|
| H A D | Term.sml | 170 let val (ty1,ty2) = with_exn Type.dom_rng typ err value
[all...] |
| /seL4-l4v-master/HOL4/src/update/ |
| H A D | updateLib.sml | 339 val (ty1, ty2) = value
|
| /seL4-l4v-master/HOL4/src/floating-point/ |
| H A D | binary_ieeeSyntax.sml | 152 val (ty1, ty2) = dest_float_ty (Term.type_of tm2) value
168 val (ty1, ty2) = dest_float_ty (Term.type_of tm2) value
|
| H A D | machine_ieeeLib.sml | 137 val ty1 = rounding_ty --> fp_ty --> int_option_ty value
148 val ty1 = value
175 val ty1 = fp_ty --> Type.bool value
206 val ty1 = value
234 val ty1 value
253 val ty1 = value
348 val (ty1, ty2) = Type.dom_rng (Term.type_of float_to_fp) value
[all...] |
| /seL4-l4v-master/HOL4/examples/dev/ |
| H A D | compile.sml | 62 let val ty1 = fst(dom_rng(type_of tm1)) value
1882 val (ty1,ty2) = dom_rng ty value
1909 val (ty1,ty value
1973 let val (ty1,ty2) = dom_rng(type_of tm1) value
1986 then let val (ty1,ty2) = dest_prod ty value
2007 val (ty1,ty2) = dom_rng fty value
[all...] |
| /seL4-l4v-master/HOL4/src/list/src/ |
| H A D | listSyntax.sml | 99 let val (ty1,ty2) = pairSyntax.dest_prod (eltype l) value
|
| /seL4-l4v-master/HOL4/src/holyhammer/ |
| H A D | hhExportTh0.sml | 35 let val (ty1,ty2) = pair_of_list Args in value
515 let val (ty1,ty2) = pair_of_list Args in value
|
| /seL4-l4v-master/HOL4/src/num/termination/ |
| H A D | TotalDefn.sml | 77 let val ty1 = fst(dom_rng(type_of R)) value
|
| /seL4-l4v-master/HOL4/src/1/ |
| H A D | TypeBasePure.sml | 891 let val ty1 = type_of tm value
|
| /seL4-l4v-master/HOL4/src/0/ |
| H A D | Term.sml | 465 let val (ty1,ty2) = with_exn Type.dom_rng typ err value
[all...] |
| /seL4-l4v-master/HOL4/examples/l3-machine-code/common/ |
| H A D | Import.sml | 868 val ty1 = Term.type_of tm value
[all...] |