Searched refs:mk_var (Results 126 - 150 of 368) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/src/coretypes/
H A DPairRules.sml97 val gfinst = mk_var(fst(dest_var gf),fty)
103 val gxinst = mk_var(fst(dest_var gx),xty)
104 and gyinst = mk_var(fst(dest_var gy),yty)
113 val gpinst = mk_var(fst (dest_var gp),pty)
144 val gfinst = mk_var(fst(dest_var gf), fty)
147 val gxinst = mk_var(fst(dest_var gx), xty)
148 and gyinst = mk_var(fst(dest_var gy), yty)
1500 val f = mk_var("f", alpha --> bool)
1501 val x = mk_var("x", alpha)
1520 val gxinst = mk_var((fs
[all...]
H A DpairTools.sml21 val mk_var = variant fvs o mk_var value
29 val v = mk_var((name_of v)^s,ty)
33 (fn()=> rename_tac v (mk_var(sv^(Int.toString(n())),ty)))
/seL4-l4v-10.1.1/HOL4/src/monad/more_monads/
H A Dselftest.sml91 hd args = mk_var("opt", ``:num option``) andalso
/seL4-l4v-10.1.1/HOL4/src/pattern_matches/
H A DpatternMatchesSyntax.sml33 fn ty => mk_var (next_name (), ty)
265 variant (free_varsl tl) (mk_var("_uv", oneSyntax.one_ty))
308 val mk_var = mk_var_gen "v" avoid value
318 mk_wc (type_of v) else mk_var (type_of v)
357 AP_THM combinTheory.K_DEF (mk_var("x", alpha))
620 val x = mk_var ("x", type_of p)
757 fun mk_fake wc = mk_var (GrammarSpecials.mk_fakeconst_name {fake = "_", original = NONE}, type_of wc)
763 variant (free_varsl [pat, guard, rh]) (mk_var("_", oneSyntax.one_ty))
859 val args = Lib.mapi (fn i => fn ty => mk_var("x" ^ Int.toString i, ty)) argtys
/seL4-l4v-10.1.1/HOL4/src/tfl/src/
H A DwfrecUtils.sml111 fn ty => mk_var(pass "v", ty)
H A DDefn.sml86 let val P = mk_var("P",bool)
87 val Q = mk_var("Q",bool)
88 val R = mk_var("R",bool)
313 let val M = mk_var("M",bool)
314 val P = mk_var("P",bool)
315 val M1 = mk_var("M1",bool)
685 val fvar = mk_var(fst(dest_var f),
717 val aux_fvar = mk_var(aux_name,itlist(curry(op-->)) (map type_of (R1::SV)) Ty)
748 val fvar = mk_var(fst(dest_var f),
864 val nvs = map (curry mk_var "
[all...]
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/translations/
H A DtranslationsLib.sml839 ((mk_var ("f", ltl_type --> num)) |-> f_term)] new_f_term;
860 val pos_start_term = subst [mk_var("l", type_of var_list_term) |-> var_list_term] pos_start_term;
872 val pos_start_term_concr = subst [mk_var("l", type_of var_list_term) |-> var_list_term] pos_start_term_concr
875 val pos_start_thm_concr = GEN (mk_var ("x", ltl_type)) pos_start_thm_concr;
914 (subst [(mk_var("f", ltl_type --> num) |-> f_term),
915 (mk_var("y", num) |-> term_of_int used_vars_num),
916 (mk_var("n", num) |-> term_of_int n),
917 (mk_var("e", ltl_type) |-> t),
918 (mk_var("m", num --> num) |-> et)] renaming_cond)
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/
H A DtestACL2encoding.ml170 (REFL o curry mk_var "a") ``:'a list``);
175 (REFL o curry mk_var "a") ``:'a + num``);
180 (REFL o curry mk_var "a") ``:(num + 'a) list``);
185 (REFL o curry mk_var "a") ``:('a + num) list``);
H A DtranslateLib.sml78 then mk_var(prime((fst o dest_var o var) thm),
81 (mk_var("x",(type_of o sexp_to_term) thm))
/seL4-l4v-10.1.1/HOL4/src/quotient/src/
H A Dquotient.sml195 map Psyntax.mk_var (zip nms tylist)
289 val r = Term.variant (free_vars REL) (mk_var{Name="r", Ty=ty})
293 val c = Term.variant (free_vars rcl) (mk_var{Name="c", Ty=cty})
296 val x = Term.variant (free_vars P) (mk_var{Name="x", Ty=ty})
418 val ty_REP = mk_var{Name = rep,
431 val ty_ABS = mk_var{Name = abs,
442 val r'tm = mk_var{Name="r'", Ty=ty}
447 val atm = mk_var{Name="a", Ty=nty}
482 val x = mk_var{Name="x", Ty=cty}
483 val y = mk_var{Nam
[all...]
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/
H A DfuncCall.sml110 (mk_plet (mk_var("m" ^ Int.toString(slot) , !VarType), mk_atom r, e), slot + 1))
117 (mk_plet (r, mk_atom (mk_var("m" ^ Int.toString(slot), !VarType)), e), slot + 1))
H A Drefine.sml97 (mk_var("v"^Int.toString i,type_of b),p)) plist'
100 val vb4 = mk_var("v"^Int.toString(length plist''), type_of b4)
/seL4-l4v-10.1.1/HOL4/src/floating-point/
H A Dbinary_ieeeSyntax.sml77 fun mk_float_var tw = fn v => Term.mk_var (v, mk_float_ty tw)
78 fun mk_ifloat_var tw = fn v => Term.mk_var (v, mk_ifloat_ty tw)
/seL4-l4v-10.1.1/HOL4/src/new-datatype/
H A DWitness.sml100 (mk_var ("x", (fst o dom_rng o type_of) tm))
171 (mk_var ("x", type_of b))
/seL4-l4v-10.1.1/HOL4/src/postkernel/
H A DThyDataSexp.sml136 | Type ty => Term.mk_var("x", ty) :: acc
204 | Type ty => "Y" ^ StringData.encode (tmw (Term.mk_var("x", ty)))
/seL4-l4v-10.1.1/HOL4/src/quantHeuristics/
H A DquantHeuristicsLibParameters.sml62 val vars = map (fn (n, ty) => (mk_var (vn^"_"^(Int.toString n), ty))) ntL
342 fun mk_new_var (s, ty) = mk_var (s, ty);
H A Dselftest.sml69 val x = mk_var ("x", numLib.num);
82 val x = mk_var ("x", numLib.num);
/seL4-l4v-10.1.1/HOL4/src/simp/src/
H A DcongLib.sml62 val var = mk_var ("x", hol_type)
75 val var = mk_var ("x", hol_type)
/seL4-l4v-10.1.1/graph-refine/
H A Dpseudo_compile.py16 (mk_var, mk_plus, mk_uminus, mk_minus, mk_times, mk_modulus, mk_bwand, mk_eq,
40 return mk_var (v_nm, typ)
92 return mk_var (v_nm, typ)
94 vs = [(mk_word32 (j), mk_var (v_nm, typ))
/seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/
H A Dcodegen_x86Lib.sml17 fun foo (i,s) = mk_var("r" ^ int_to_string i,``:word32``) |-> mk_var(s, ``:word32``)
/seL4-l4v-10.1.1/HOL4/examples/ARM/v4/
H A Darm_emitScript.sml54 FAIL num2register ^(mk_var("30 < n",bool)) n`,
75 FAIL num2condition ^(mk_var("15 < n",bool)) n`,
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/Examples/KatiPuzzle/
H A DKatiPuzzleScript.sml76 (fn s => mk_var(s,bool))
167 (mk_var("s",type_of s))
/seL4-l4v-10.1.1/HOL4/src/HolSmt/
H A DSmtLib_Parser.sml200 (fn (s, t) => (s, Term.mk_var (s, Term.type_of t), t)) bindings
242 val vars = List.map (fn vT => (Lib.fst vT, Term.mk_var vT)) vars
393 val tm = Term.mk_var (name,
412 val vars = List.map (fn vT => (Lib.fst vT, Term.mk_var vT)) vars
425 val tm = Term.mk_var (name,
/seL4-l4v-10.1.1/HOL4/src/integer/
H A DOmegaSymbolic.sml49 val pvar = mk_var("p", bool)
50 val qvar = mk_var("q", bool)
51 val xvar = mk_var("x", int_ty)
170 val p = mk_var("p", c_ty)
207 (REWRITE_RULE [nilth] (INST [mk_var(varname, clist_ty) |-> nil_t] consth),
/seL4-l4v-10.1.1/HOL4/examples/lambda/basics/
H A DtermScript.sml29 val LAM_t = mk_var("LAM", ``:string -> ^newty -> ^newty``)
39 val APP_t = mk_var("APP", ``:^newty -> ^newty -> ^newty``)
53 val VAR_t = mk_var("VAR", ``:string -> ^newty``)
89 val t = mk_var("t", newty)
134 val t = mk_var("t", ty)

Completed in 407 milliseconds

1234567891011>>