DependentInductiveTypes

FrapWithoutSets.v

@@ -387,3 +387,10 @@ Proof.
   simplify.
   apply includes_intro; auto.
 Qed.
+
+Ltac dep_cases E :=
+  let x := fresh "x" in
+    remember E as x; simpl in x; dependent destruction x;
+      try match goal with
+            | [ H : _ = E |- _ ] => try rewrite <- H in *; clear H
+          end.

README.md

@@ -31,4 +31,4 @@ The main narrative, also present in the book PDF, presents standard program-proo
 
 There are also two supplementary files that are independent of the main narrative, for introducing programming with dependent types, a distinctive Coq feature that we neither use nor recommend for the problem sets, but which many students find interesting (and useful in other contexts).
 * `SubsetTypes.v`: a first introduction to dependent types by attaching predicates to normal types (used after `CompilerCorrectness.v` in the last course offering)
-* One more coming soon
+* `DependentInductiveTypes.v`: building type dependency into datatype definitions (used after `LambdaCalculusAndTypeSoundness.v` in the last course offering)

_CoqProject

@@ -36,6 +36,7 @@ SubsetTypes.v
 SubsetTypes_template.v
 LambdaCalculusAndTypeSoundness_template.v
 LambdaCalculusAndTypeSoundness.v
+DependentInductiveTypes.v
 TypesAndMutation.v
 DeepAndShallowEmbeddings_template.v
 DeepAndShallowEmbeddings.v