216 | _ => warns |
216 | _ => warns |
217 |
217 |
218 val warns = map_check_aux rty [] |
218 val warns = map_check_aux rty [] |
219 in |
219 in |
220 if null warns then () |
220 if null warns then () |
221 else warning ("No map function defined for " ^ (commas warns) ^ |
221 else warning ("No map function defined for " ^ commas warns ^ |
222 ". This will cause problems later on.") |
222 ". This will cause problems later on.") |
223 end |
223 end |
224 |
224 |
225 |
225 |
226 |
226 |
227 (*** interface and syntax setup ***) |
227 (*** interface and syntax setup ***) |
228 |
228 |
229 |
229 |
230 (* the ML-interface takes a list of 5-tuples consisting of |
230 (* the ML-interface takes a list of 5-tuples consisting of: |
231 |
231 |
232 - the name of the quotient type |
232 - the name of the quotient type |
233 - its free type variables (first argument) |
233 - its free type variables (first argument) |
234 - its mixfix annotation |
234 - its mixfix annotation |
235 - the type to be quotient |
235 - the type to be quotient |
236 - the relation according to which the type is quotient |
236 - the relation according to which the type is quotient |
237 |
237 |
238 it opens a proof-state in which one has to show that the |
238 it opens a proof-state in which one has to show that the |
239 relations are equivalence relations |
239 relations are equivalence relations |
240 *) |
240 *) |
241 |
241 |
242 fun quotient_type quot_list lthy = |
242 fun quotient_type quot_list lthy = |
243 let |
243 let |
244 (* sanity check *) |
244 (* sanity check *) |