[isabelle] Be nice to have short tutorials on Quotient Types and Lifting

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 MHonArc.