/seL4-l4v-master/HOL4/src/0/ |
H A D | Type.sig | 1 signature Type = signature
|
/seL4-l4v-master/HOL4/src/datatype/mutrec/ |
H A D | TypeInfo.sig | 3 datatype type_info = existing of Type.hol_type
|
H A D | TypeInfo.sml | 3 datatype type_info = existing of Type.hol_type
|
/seL4-l4v-master/HOL4/src/experimental-kernel/ |
H A D | Type.sig | 1 signature Type = signature
|
H A D | Term.sig | 4 include FinalTerm where type hol_type = Type.hol_type
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | type_pp.sig | 5 Type.hol_type -> term_pp_types.uprinter 7 int -> Type.hol_type -> term_pp_types.uprinter
|
H A D | Pretype.sig | 33 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 D | type_grammar.sig | 12 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 D | typecheck_error.sml | 4 ConstrainFail of Term.term * Type.hol_type * string 6 | OvlNoType of string * Type.hol_type
|
H A D | term_pp_types.sml | 19 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 D | type_grammar_dtype.sml | 16 | TYABBREV of KernelSig.kernelname * Type.hol_type * bool
|
/seL4-l4v-master/HOL4/help/src-sml/ |
H A D | Symbolic.sml | 4 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 D | while_langScript.sml | 5 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 D | ARM_proverLib.sig | 13 val get_monad_type : Type.hol_type -> Type.hol_type 16 val get_type_inst : Type.hol_type * bool -> Type.hol_type
|
H A D | ARM_prover_extLib.sig | 13 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 D | caseEqAbbrevScript.sml | 5 Type foo = ���:'a list���
|
/seL4-l4v-master/HOL4/src/thm/ |
H A D | Overlay.sml | 25 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 D | state_transformerSyntax.sml | 23 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 D | armSyntax.sml | 31 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 D | armSyntax.sml | 31 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 D | wordsSyntax.sml | 15 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 D | fcpLib.sml | 38 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 D | SharingTables.sig | 27 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 D | file_readerLib.sig | 20 val tysize : unit -> Type.hol_type 21 val wsize : unit -> Type.hol_type
|
/seL4-l4v-master/HOL4/src/integer/ |
H A D | integer_wordSyntax.sml | 28 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))
|