Searched refs:Type (Results 76 - 100 of 497) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/src/boss/ml_evaluation/
H A DLift.sml24 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 DConstMapML.sig6 type hol_type = Type.hol_type
/seL4-l4v-10.1.1/HOL4/src/list/src/
H A DnumposrepLib.sml9 val (Type, Term) = parse_from_grammars numposrepTheory.numposrep_grammars value
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DfolMapping.sig13 type hol_type = Type.hol_type
/seL4-l4v-10.1.1/HOL4/src/monad/more_monads/
H A Dstate_monadLib.sml9 val (Type, Term) = value
/seL4-l4v-10.1.1/HOL4/src/n-bit/
H A DbitstringSyntax.sml27 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 DHol_pp.sig3 type hol_type = Type.hol_type
H A DParseDatatype_dtype.sml7 | dAQ of Type.hol_type
/seL4-l4v-10.1.1/HOL4/src/postkernel/
H A DTheoryLexer.sml11 open Feedback Lib Type Term Thm
/seL4-l4v-10.1.1/HOL4/src/proofman/tests/
H A Dselftest.sml17 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 DstringLib.sml23 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 DType.sml2 (* 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 DTerm.sml24 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 Dnomdatatype.sml53 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 DutilsLib.sml14 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 DmechReasoning.sml62 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 Dmake_iss.sml139 \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 Dexport_theory.scala67 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 Dexport_theory.scala67 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 DPrim_rec.sml35 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 DsumScript.sml262 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 Dmachine_ieeeLib.sml10 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 DwfrecUtils.sml80 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 Duser_lemma_primitive_operationsScript.sml523 (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 DSmtLib_Parser.sml111 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...]

Completed in 226 milliseconds

1234567891011>>