/seL4-l4v-10.1.1/HOL4/src/boss/ml_evaluation/ |
H A D | Lift.sml | 24 val list_mk_comb_var = mk_var("list_mk_comb", Type`:'term -> 'term`) 25 val cons_var = mk_var ("cons",Type`:'term -> 'term -> 'term`) 26 val nil_var = mk_var ("nil",Type`:'term`) 27 val comma_var = mk_var (",",Type`:'term -> 'term -> 'term`)
|
/seL4-l4v-10.1.1/HOL4/src/emit/ |
H A D | ConstMapML.sig | 6 type hol_type = Type.hol_type
|
/seL4-l4v-10.1.1/HOL4/src/list/src/ |
H A D | numposrepLib.sml | 9 val (Type, Term) = parse_from_grammars numposrepTheory.numposrep_grammars value
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | folMapping.sig | 13 type hol_type = Type.hol_type
|
/seL4-l4v-10.1.1/HOL4/src/monad/more_monads/ |
H A D | state_monadLib.sml | 9 val (Type, Term) = value
|
/seL4-l4v-10.1.1/HOL4/src/n-bit/ |
H A D | bitstringSyntax.sml | 27 Term.mk_comb (Term.inst [Type.alpha |-> ty] tm, v)} 110 val bitstring_ty = listSyntax.mk_list_type Type.bool 192 fun mk_bit n = Term.mk_var ("b" ^ Int.toString n, Type.bool) 197 (List.tabulate (w, fn i => mk_bit (w - i - 1 + n)), Type.bool)
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | Hol_pp.sig | 3 type hol_type = Type.hol_type
|
H A D | ParseDatatype_dtype.sml | 7 | dAQ of Type.hol_type
|
/seL4-l4v-10.1.1/HOL4/src/postkernel/ |
H A D | TheoryLexer.sml | 11 open Feedback Lib Type Term Thm
|
/seL4-l4v-10.1.1/HOL4/src/proofman/tests/ |
H A D | selftest.sml | 17 if xv |> type_of |> Type.polymorphic then OK() 21 val _ = tprint "Type parsing with newlines" 25 val _ = if Type.compare(ty,Type.alpha) = EQUAL then OK()
|
/seL4-l4v-10.1.1/HOL4/src/string/ |
H A D | stringLib.sml | 23 fun refl_clause ty = Thm.INST_TYPE [Type.alpha |-> ty] boolTheory.REFL_CLAUSE 44 val inst_to_string = Thm.INST_TYPE [Type.alpha |-> stringSyntax.char_ty] 140 val name = "string2" ^ fst (Type.dest_type ty) 153 val name = fst (Type.dest_type ty) ^ "2string"
|
/seL4-l4v-10.1.1/HOL4/src/0/ |
H A D | Type.sml | 2 (* FILE : Type.sml *) 7 (* UPDATE : October 94. Type signature implementation moved from *) 14 structure Type :> Type = structure 21 val ERR = mk_HOL_ERR "Type"; 22 val WARN = HOL_WARNING "Type"; 162 * Type variables * 325 end (* Type *)
|
H A D | Term.sml | 24 val --> = Type.-->; infixr 3 -->; 36 val hty = if Type.polymorphic ty then POLY ty else GRND ty 52 open KernelSig Type 106 | ty_of (Comb(Rator, _)) E = snd(Type.dom_rng(ty_of Rator E)) 130 local fun tyV (Fv(_,Ty)) k = k (Type.type_vars Ty) 133 | tyV (Const(_,POLY Ty)) k = k (Type.type_vars Ty) 194 of EQUAL => Type.compare (ty1,ty2) 221 of EQUAL => Type.compare (to_hol_type ty1, 231 Abs(Fv(_, ty2),N)) => (case Type.compare(ty1,ty2) 389 fun ground x = Lib.all (fn {redex,residue} => not(Type [all...] |
/seL4-l4v-10.1.1/HOL4/examples/lambda/basics/ |
H A D | nomdatatype.sml | 53 val _ = Type.compare(type_of v, stringSyntax.string_ty) = EQUAL orelse 160 if Type.compare(type_of v, repty) = EQUAL then 174 val f = mk_var("f", r --> Type.gen_tyvar()) 185 val o_t = combinSyntax.o_tm |> inst [alpha |-> Type.gen_tyvar()] 214 if Type.compare(ty1,ty2) = EQUAL then EQUAL 215 else if Type.compare(ty1,``:string``) = EQUAL then LESS 217 else Type.compare(ty1, ty2)
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
H A D | utilsLib.sml | 14 val (Type,Term) = parse_from_grammars wordsTheory.words_grammars value 212 val dom = fst o Type.dom_rng 213 val rng = snd o Type.dom_rng 501 (n + 1, fn j => Term.mk_var ("v" ^ Int.toString j, Type.alpha)) 524 val {Thy, Tyop, ...} = Type.dest_thy_type ty 530 val kv = Term.inst [Type.beta |-> fld_ty] 555 ty1 = ty2 andalso (ty3 = Type.bool orelse ty3 = ty1) 615 val {Thy, Tyop, ...} = Type.dest_thy_type ty 640 val term_rng = snd o Type.dom_rng o Term.type_of 696 val m = Type [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | mechReasoning.sml | 62 val changed_list = mk_list (mreg_list, Type`:MREG`); 110 mk_var ("v" ^ (i := !i + 1; Int.toString (!i)) , Type `:DATA`) 192 fun new_var() = (i := !i + 1; mk_var ("v"^Int.toString (!i), Type`:DATA`)) 344 let val st = mk_pair (mk_var ("regs", Type `:REGISTER |-> DATA`), 345 mk_var ("mem", Type `:ADDR |-> DATA`)) 393 val st' = mk_var ("st", Type `:DSTATE`); 464 val ir_abbr = mk_var ("ir", Type `:CTL_STRUCTURE`); 569 val ir_abbr = mk_var ("ir", Type `:CTL_STRUCTURE`); 570 val st = mk_var ("st", Type `:DSTATE`); 648 val ir_abbr = mk_var ("ir", Type ` [all...] |
/seL4-l4v-10.1.1/HOL4/tools/ |
H A D | make_iss.sml | 139 \Type: filesandordirs; Name: \"{app}\\tools\"\n\ 140 \Type: filesandordirs; Name: \"{app}\\help\"\n\ 141 \Type: files; Name: \"{app}\\config-override\"\n"
|
/seL4-l4v-10.1.1/isabelle/src/Pure/Thy/ |
H A D | export_theory.scala | 67 types: List[Type], 153 sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ]) 155 def cache(cache: Term.Cache): Type = 156 Type(entity.cache(cache), 161 def read_types(provider: Export.Provider): List[Type] = 170 Type(entity, args, abbrev)
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Thy/ |
H A D | export_theory.scala | 67 types: List[Type], 153 sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ]) 155 def cache(cache: Term.Cache): Type = 156 Type(entity.cache(cache), 161 def read_types(provider: Export.Provider): List[Type] = 170 Type(entity, args, abbrev)
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | Prim_rec.sml | 35 val (Type,Term) = parse_from_grammars boolTheory.bool_grammars value 73 val pat_type = List.foldr tmlist_type Type.bool patvars 74 val inst_type = List.foldr tmlist_type Type.bool instvars 75 val tyinst = Type.match_type pat_type inst_type 425 let val (dty,rty) = Type.dom_rng ty 638 local val boolvar = genvar Type.bool 707 val v = genvar Type.bool 829 local val v = genvar Type.bool 872 local val v = genvar Type.bool 916 local val v = genvar Type [all...] |
/seL4-l4v-10.1.1/HOL4/src/coretypes/ |
H A D | sumScript.sml | 262 let val inst = INST_TYPE [Type.gamma |-> Type.bool] sum_axiom 278 let val inst = INST_TYPE [Type.gamma |-> Type.bool] sum_axiom 294 let val inst = INST_TYPE [Type.gamma |-> Type.alpha] sum_axiom 310 let val inst = INST_TYPE [Type.gamma |-> Type.beta] sum_axiom
|
/seL4-l4v-10.1.1/HOL4/src/floating-point/ |
H A D | machine_ieeeLib.sml | 10 val (Type, Term) = parse_from_grammars binary_ieeeTheory.binary_ieee_grammars value 38 case Lib.total Type.dest_type ty of 175 val ty1 = fp_ty --> Type.bool 176 val ty2 = float_ty --> Type.bool 191 val ty = Type.mk_type ("itself", [dim_ty]) --> float_ty 348 val (ty1, ty2) = Type.dom_rng (Term.type_of float_to_fp) 396 val float_ty = Type.mk_type ("float", [t_ty, w_ty]) 422 val lift2b = lift2b fp_to_float fp_ty float_ty Type.bool
|
/seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
H A D | wfrecUtils.sml | 80 if type_of tm = Type.bool 116 fun match_type thry ty1 ty2 = Type.match_type ty1 ty2;
|
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/ |
H A D | user_lemma_primitive_operationsScript.sml | 523 (INST_TYPE [alpha |-> Type `:word32`, beta |-> Type `:word32`, gamma |-> alpha] read_cpsr_triple_par_effect_fixed_lem) 530 (INST_TYPE [alpha |-> Type `:word32`, beta |-> Type `:word32`, gamma |-> alpha] read_cpsr_triple_par_effect_fixed_lem) 545 (INST_TYPE [alpha |-> Type `:CP15sctlr`, beta |-> Type `:CP15scr`, gamma |-> alpha] read_cpsr_triple_par_effect_fixed_lem2) 552 (INST_TYPE [alpha |-> Type `:CP15sctlr`, beta |-> Type `:CP15scr`, gamma |-> alpha] read_cpsr_triple_par_effect_fixed_lem2) 567 (INST_TYPE [alpha |-> Type `:word32`, beta |-> Type ` [all...] |
/seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
H A D | SmtLib_Parser.sml | 111 fun parse_type_operands get_token tydict acc : Type.hol_type list = 126 and parse_compound_type get_token tydict (token : string) : Type.hol_type = 135 : Type.hol_type list -> Type.hol_type = 153 : Type.hol_type list -> Type.hol_type = 159 fun parse_type get_token tydict : Type.hol_type = 162 fun parse_type_list get_token tydict : Type.hol_type list = 216 and parse_sorted_vars get_token tydict : (string * Type.hol_type) list = 376 val ty = Type [all...] |