WIP

braibant · Mar 22, 2013 · 20f9c07 · 20f9c07
1 parent 009051e
commit 20f9c07
Showing 1 changed file with 13 additions and 1 deletion.
diff --git a/test.v b/test.v
@@ -80,7 +80,19 @@ Show Proof.
 Qed.  
 End sec_absu_2ismul3.
 
-
+Section vect. 
+  Variable A : Type. 
+  Inductive vector : nat -> Type :=
+    | nil : vector 0
+    | cons : forall n, A -> vector n -> vector (S n). 
+
+
+  Goal forall v : vector 0, v = nil. 
+  intros. 
+  Fail invert v. 
+  Abort. 
+End vect. 
+
 
 Inductive tm : Type :=
   | const : nat -> tm