[isabelle] char :: full_exhaustive
- To: isabelle-users at cl.cam.ac.uk
- Subject: [isabelle] char :: full_exhaustive
- From: Lars Hupel <hupel at in.tum.de>
- Date: Tue, 20 Dec 2016 17:50:42 +0100
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.5.1
you changed the representation of characters a while back, but it seems
like the Quickcheck setup is lacking a "full_exhaustive" instance.
The stupidest possible workaround is
quickcheck_generator char constructors: char_of_nat
... which I have just added locally to my theories.
Maybe we should think about a proper implementation.
This archive was generated by a fusion of
Pipermail (Mailman edition) and