Searched refs:Type (Results 1 - 25 of 548) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/src/0/
H A DType.sig1 signature Type = signature
/seL4-l4v-master/HOL4/src/datatype/mutrec/
H A DTypeInfo.sig3 datatype type_info = existing of Type.hol_type
H A DTypeInfo.sml3 datatype type_info = existing of Type.hol_type
/seL4-l4v-master/HOL4/src/experimental-kernel/
H A DType.sig1 signature Type = signature
H A DTerm.sig4 include FinalTerm where type hol_type = Type.hol_type
/seL4-l4v-master/HOL4/src/parse/
H A Dtype_pp.sig5 Type.hol_type -> term_pp_types.uprinter
7 int -> Type.hol_type -> term_pp_types.uprinter
H A DPretype.sig33 val fromType : Type.hol_type -> pretype
37 val clean : pretype -> Type.hol_type
38 val toTypeM : pretype -> Type.hol_type in_env
39 val toType : pretype -> Type.hol_type
45 val typantiq_constructors : (pretype,Type.hol_type) parse_type.tyconstructors
H A Dtype_grammar.sig12 val structure_to_type : type_structure -> Type.hol_type
22 val abb_dest_type : grammar -> Type.hol_type ->
24 Args : Type.hol_type list}
39 val new_abbreviation : {knm : kernelname, ty : Type.hol_type, print : bool} ->
52 : (grammar -> Type.hol_type -> HOLPP.pretty) -> unit
H A Dtypecheck_error.sml4 ConstrainFail of Term.term * Type.hol_type * string
6 | OvlNoType of string * Type.hol_type
H A Dterm_pp_types.sml19 BV of Type.hol_type * (unit -> string)
20 | FV of Type.hol_type * (unit -> string)
24 | Const of {Thy:string,Name:string,Ty:Type.hol_type * (unit -> string)}
25 | SymConst of {Thy:string,Name:string,Ty:Type.hol_type * (unit -> string)}
H A Dtype_grammar_dtype.sml16 | TYABBREV of KernelSig.kernelname * Type.hol_type * bool
/seL4-l4v-master/HOL4/help/src-sml/
H A DSymbolic.sml4 val symb_map = [("Type", "-->", "arrow"),
13 fun unsymb "Type.-->" = "Type.arrow"
26 fun tosymb "Type.arrow" = "Type.-->"
/seL4-l4v-master/HOL4/examples/Hoare-for-divergence/
H A Dwhile_langScript.sml5 Type nat[pp] = ���:num���;
9 Type name = ���: string ���
10 Type value = ���: nat ���
11 Type store = ���: name -> value ���
12 Type exp = ���: store -> value ���
26 Type output = ���: value list ���
27 Type state[pp] = ���: store # output ���
/seL4-l4v-master/HOL4/examples/ARM_security_properties/
H A DARM_proverLib.sig13 val get_monad_type : Type.hol_type -> Type.hol_type
16 val get_type_inst : Type.hol_type * bool -> Type.hol_type
H A DARM_prover_extLib.sig13 val get_monad_type : Type.hol_type -> Type.hol_type
20 val get_type_inst : Type.hol_type * bool -> Type.hol_type
/seL4-l4v-master/HOL4/src/boss/theory_tests/
H A DcaseEqAbbrevScript.sml5 Type foo = ���:'a list���
/seL4-l4v-master/HOL4/src/thm/
H A DOverlay.sml25 structure Type : FinalType structure
26 structure Term : FinalTerm where type hol_type = Type.hol_type
29 and type hol_type = Type.hol_type
36 structure Type = Type structure
/seL4-l4v-master/HOL4/src/monad/more_monads/
H A Dstate_transformerSyntax.sml23 val (ty1, ty2) = Lib.with_exn Type.dom_rng ty err
31 val state_ty = Type.mk_vartype "'state"
37 tm2 |> Term.type_of |> Type.dom_rng |> fst))
40 (Term.inst [Type.alpha |-> ty, Type.beta |-> Term.type_of tm2] tm1,
55 (Term.inst [Type.alpha |-> ty1,
56 Type.beta |-> ty,
68 val get_state_ty = fst o Type.dom_rng o snd o Type.dom_rng o Term.type_of
94 Term.mk_comb (Term.inst [Type
[all...]
/seL4-l4v-master/HOL4/examples/ARM_security_properties/model/
H A DarmSyntax.sml31 Term.inst [Type.alpha |->
94 Term.inst [Type.alpha |-> stringSyntax.string_ty] s)
99 [Type.alpha |-> Term.type_of v,
100 Type.beta |-> Term.type_of s] valuestate_tm, [v,s])
104 HolKernel.mk_comb(Term.inst[Type.alpha |-> Term.type_of t] constT_tm,t)
109 [Type.alpha |-> dest_monad_type (Term.type_of f),
110 Type.beta |-> (dest_monad_type o snd o Type.dom_rng o Term.type_of) g]
116 [Type.alpha |-> dest_monad_type (Term.type_of f),
117 Type
[all...]
/seL4-l4v-master/HOL4/examples/ARM/v7/
H A DarmSyntax.sml31 Term.inst [Type.alpha |->
93 Term.inst [Type.alpha |-> stringSyntax.string_ty] s)
98 [Type.alpha |-> Term.type_of v,
99 Type.beta |-> Term.type_of s] valuestate_tm, [v,s])
103 HolKernel.mk_comb(Term.inst[Type.alpha |-> Term.type_of t] constT_tm,t)
108 [Type.alpha |-> dest_monad_type (Term.type_of f),
109 Type.beta |-> (dest_monad_type o snd o Type.dom_rng o Term.type_of) g]
115 [Type.alpha |-> dest_monad_type (Term.type_of f),
116 Type
[all...]
/seL4-l4v-master/HOL4/src/n-bit/
H A DwordsSyntax.sml15 fun mk_word_type ty = fcpSyntax.mk_cart_type (Type.bool, ty)
22 val _ = a = Type.bool orelse
40 (Term.inst [Type.alpha |-> Type.bool, Type.beta |-> dim_of w] fcp_index_tm,
57 (fn tm => fn ty => Term.inst [Type.alpha |-> ty] tm)
69 Term.mk_comb (Term.inst [Type.alpha |-> ty] tm, boolSyntax.mk_itself ty))
142 Term.mk_comb (Term.inst [Type.alpha |-> dim_of w] tm,
158 Term.mk_comb (Term.inst [Type.alpha |-> dim_of a] tm,
168 (fn tm => fn (w, ty) => Term.mk_comb (Term.inst [Type
[all...]
H A DfcpLib.sml38 fun conv n = INDEX_CONV o Term.inst [Type.alpha |-> index_type n]
40 fun DIMINDEX n = conv n (fcpSyntax.mk_dimindex Type.alpha)
42 Type.alpha
51 (Thm.MP (Thm.INST_TYPE [Type.alpha |-> index_type n]
70 val _ = Type.polymorphic ty orelse raise ERR "infer_fcp_type" ""
/seL4-l4v-master/HOL4/src/postkernel/
H A DSharingTables.sig27 tymap : (Type.hol_type, int)Map.dict,
46 val make_shared_type : Type.hol_type -> stringtable -> idtable -> typetable ->
56 Type.hol_type Vector.vector
58 val build_term_vector : id Vector.vector -> Type.hol_type Vector.vector ->
65 named_types : (string * Type.hol_type) list,
66 unnamed_types : Type.hol_type list,
70 val add_types : Type.hol_type list -> sharing_data_in -> sharing_data_in
73 val write_type : sharing_data_in -> Type.hol_type -> int
80 (int -> string) * (int -> id) * Type.hol_type Vector.vector -> unit} ->
/seL4-l4v-master/HOL4/examples/machine-code/graph/
H A Dfile_readerLib.sig20 val tysize : unit -> Type.hol_type
21 val wsize : unit -> Type.hol_type
/seL4-l4v-master/HOL4/src/integer/
H A Dinteger_wordSyntax.sml28 Term.mk_comb (Term.inst [Type.alpha |-> ty] tm, boolSyntax.mk_itself ty))
38 (fn tm => fn (w, ty) => Term.mk_comb (Term.inst [Type.alpha |-> ty] tm, w))
53 Term.mk_comb (Term.inst [Type.alpha |-> wordsSyntax.dim_of w,
54 Type.beta |-> ty] tm, w))

Completed in 193 milliseconds

1234567891011>>