Lines Matching defs:types
1 (* In order to use our recursive theorem on mutually recursive types to
2 define functions on these types, we need to be able to extract from a
6 constants, one for each constructor of the mutually recursive types,
207 (* get_type_info just gets a list of the types involved in the
219 recursive types *)
220 val types = get_types (cons_data, Type`:num`, [])
293 (* get_result_typevar destructs function types until it finds that
357 recursive types *)
385 types we're defining funtions on, and if so, whether the person is
386 defining a function on it and what the domain and range types of
423 recursive (one of the types defined in the recursive type def)
524 where N is the number of mutually recursive types, fI is the
525 function defined for type I (using the order in which the types
538 (those that refer to types the user isn't defining a function for),