Nitpick: show "..." in datatype values (e.g., [{0::nat, ...}]), since these are really equivalence classes
authorblanchet
Thu May 27 17:22:16 2010 +0200 (2010-05-27)
changeset 3717038ba15040455
parent 37169 f69efa106feb
child 37171 fc1e20373e6a
Nitpick: show "..." in datatype values (e.g., [{0::nat, ...}]), since these are really equivalence classes
src/HOL/Tools/Nitpick/nitpick_model.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu May 27 16:42:03 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu May 27 17:22:16 2010 +0200
     1.3 @@ -587,7 +587,7 @@
     1.4        | term_for_rep _ seen (Type (@{type_name fun}, [T1, T2])) T'
     1.5                       (Vect (k, R')) [js] =
     1.6          term_for_vect seen k R' T1 T2 T' js
     1.7 -      | term_for_rep _ seen (Type (@{type_name fun}, [T1, T2])) T'
     1.8 +      | term_for_rep maybe_opt seen (Type (@{type_name fun}, [T1, T2])) T'
     1.9                       (Func (R1, Formula Neut)) jss =
    1.10          let
    1.11            val jss1 = all_combinations_for_rep R1
    1.12 @@ -596,7 +596,7 @@
    1.13              map (fn js => term_for_rep true seen T2 T2 (Atom (2, 0))
    1.14                                         [[int_from_bool (member (op =) jss js)]])
    1.15                  jss1
    1.16 -        in make_fun false T1 T2 T' ts1 ts2 end
    1.17 +        in make_fun maybe_opt T1 T2 T' ts1 ts2 end
    1.18        | term_for_rep maybe_opt seen (Type (@{type_name fun}, [T1, T2])) T'
    1.19                       (Func (R1, R2)) jss =
    1.20          let