[isabelle] Be nice to have short tutorials on Quotient Types and Lifting
- To: Isabelle Users ML <cl-isabelle-users at lists.cam.ac.uk>
- Subject: [isabelle] Be nice to have short tutorials on Quotient Types and Lifting
- From: Gottfried Barrow <gottfried.barrow at gmx.com>
- Date: Tue, 21 May 2013 20:24:48 -0500
- User-agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0
No one needs to respond to this, but I make this a global request,
rather than just mention it in another email I'm working on.
I've been getting some mileage out of a short example using lifting that
Brian Huffman provided me on Stackoverflow, and just using what I see in
the sources as templates, but I don't have any real understanding of
what's going on.
I'm seeing quotient types and lifting show up in lots of places, but I
haven't noticed anything in the way of tutorials, and even searches in
the collection of most documents don't return much, if anything.
In isar-ref.pdf, lifting is all through the document, which probably is
a big part of why I've been thinking I see it mentioned a lot.
It'd be nice to have something along the lines of the locales, classes,
codegen, nitpick, sledgehammer, and functions documents.
I assume no one has time. That's why I say there's no need to respond.
This archive was generated by a fusion of
Pipermail (Mailman edition) and