projects
/
coq-hetmet.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (from parent 1:
8cb9799
)
change fst_zip/snd_zip to axioms
author
Adam Megacz
<megacz@cs.berkeley.edu>
Sat, 26 Mar 2011 07:01:32 +0000
(
00:01
-0700)
committer
Adam Megacz
<megacz@cs.berkeley.edu>
Sat, 26 Mar 2011 07:01:32 +0000
(
00:01
-0700)
src/General.v
patch
|
blob
|
history
diff --git
a/src/General.v
b/src/General.v
index
6cb18be
..
25856d1
100644
(file)
--- a/
src/General.v
+++ b/
src/General.v
@@
-906,14
+906,9
@@
Lemma unleaves_injective : forall T (t1 t2:list T), unleaves t1 = unleaves t2 ->
reflexivity.
Qed.
reflexivity.
Qed.
-Lemma fst_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@fst _ _) (vec_zip v1 v2) = v1.
- admit.
- Defined.
-
-Lemma snd_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@snd _ _) (vec_zip v1 v2) = v2.
- admit.
- Defined.
-
+(* gee I wish I knew how to get Coq to accept these... *)
+Axiom fst_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@fst _ _) (vec_zip v1 v2) = v1.
+Axiom snd_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@snd _ _) (vec_zip v1 v2) = v2.
Fixpoint mapM {M}{mon:Monad M}{T}(ml:list (M T)) : M (list T) :=
match ml with
Fixpoint mapM {M}{mon:Monad M}{T}(ml:list (M T)) : M (list T) :=
match ml with