[isabelle] Quickcheck-Narrowing



Hi List.

Is there a way to extend quickcheck-narrowing for your own types,
for example the native-word types from the Native_Word library.

In attempting so, I had trouble to even define the instantiation, as all
the required types and constants are hidden with a hide_XXX command at
the end of Quickcheck_Narrowing.thy. The proof obligation reads like

instantiation
uint32 :: narrowing
narrowing_uint32 == narrowing ::
  integer \<Rightarrow> uint32 ??.Quickcheck_Narrowing.narrowing_cons


But I cannot see the type "??.Quickcheck_Narrowing.narrowing_cons" any
more.

--
  Peter





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.