reworking datatype induction. Examples

Author: philzook58

examples/README.md

@@ -0,0 +1,10 @@
+Other ideas:
+
+- <http://www.concrete-semantics.org/>
+- <https://functional-algorithms-verified.org/>
+- <https://math-comp.github.io/mcb/>
+- <http://adam.chlipala.net/cpdt/>
+- <http://adam.chlipala.net/frap/>
+- Paulson Blog Posts
+  - <https://lawrencecpaulson.github.io/2025/01/06/Code_Generation.html>
+  - <https://lawrencecpaulson.github.io/2024/12/20/Quickstart.html>

examples/leroy_compiler/README.md

@@ -0,0 +1 @@
+<https://xavierleroy.org/courses/EUTypes-2019/>

examples/soft_found/README.md

@@ -0,0 +1,3 @@
+# Software Foundations
+
+[Software Foundations](https://softwarefoundations.cis.upenn.edu/) is a famous tutorial for the [Rocq proof assistant](https://rocq-prover.org/). This is a translation from Coq to Knuckledragger.