Searched defs:constructor (Results 1 - 15 of 15) sorted by relevance

/seL4-l4v-10.1.1/HOL4/src/datatype/
H A Dind_types.sig4 type constructor = string * hol_type list type
H A DDatatype.sig9 type constructor = string * hol_type list type
H A DDatatype.sml54 type constructor = string * hol_type list type
223 fun constructor (cname, ptys) = (cname, map mk_hol_type ptys) function
[all...]
H A Dind_types.sml22 type constructor = string * hol_type list type
/seL4-l4v-10.1.1/HOL4/src/parse/
H A DParseDatatype.sig9 type constructor = ParseDatatype_dtype.constructor type
H A DParseDatatype_dtype.sml10 type constructor = string * pretype list type
/seL4-l4v-10.1.1/HOL4/src/pattern_matches/
H A DconstrFamiliesLib.sig12 type constructor type
[all...]
H A DconstrFamiliesLib.sml132 datatype constructor = CONSTR of term * (string list) type
/seL4-l4v-10.1.1/HOL4/src/HolSmt/
H A DYices.sml535 "not a data type constructor (range type is not a data type)" type
/seL4-l4v-10.1.1/HOL4/src/quantHeuristics/
H A DquantHeuristicsLibParameters.sml301 val constructor = hd (TypeBase.constructors_of ty) value
/seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/
H A DRecftn.sml600 val (constructor, _) = decompose (cons_and_args, []) value
[all...]
H A DMutRecDef.sml535 val constructor = mk_var {Name = name, Ty = constructor_type} value
[all...]
/seL4-l4v-10.1.1/HOL4/src/datatype/record/
H A DRecordType.sml167 val constructor = value
[all...]
/seL4-l4v-10.1.1/HOL4/src/quotient/src/
H A Dquotient.sml1382 "Missing quotient extension theorem for type constructor " ^ type
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/
H A DfunctionEncodeLib.sml2088 val constructor value
[all...]

Completed in 261 milliseconds