equal
deleted
inserted
replaced
336 |
336 |
337 definition |
337 definition |
338 "jad = apsnd transpose o length_permutate o map sparsify" |
338 "jad = apsnd transpose o length_permutate o map sparsify" |
339 |
339 |
340 definition |
340 definition |
341 "jad_mv v = inflate o split zip o apsnd (map listsum o transpose o map (map (\<lambda> (i, x). v ! i * x)))" |
341 "jad_mv v = inflate o case_prod zip o apsnd (map listsum o transpose o map (map (\<lambda> (i, x). v ! i * x)))" |
342 |
342 |
343 lemma "matrix (M::int list list) rs cs \<Longrightarrow> False" |
343 lemma "matrix (M::int list list) rs cs \<Longrightarrow> False" |
344 quickcheck[tester = smart_exhaustive, size = 6] |
344 quickcheck[tester = smart_exhaustive, size = 6] |
345 oops |
345 oops |
346 |
346 |