[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

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

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


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