::: for Cons in proofs (#133)

affeldt-aist · Jul 5, 2024 · 41adeb5 · 41adeb5
1 parent 9d0d02f
commit 41adeb5
Showing 1 changed file with 1 addition and 5 deletions.
diff --git a/example_typed_store.v b/example_typed_store.v
@@ -128,6 +128,7 @@ Arguments cget {ml_type N locT s T}.
 Arguments Nil {a a_1}.
 Arguments Cons {a a_1}.
 Arguments rtl {T}.
+Notation "x ':::' y" := (Cons x y) (at level 60).
 
 Lemma rtl_tl_self T (a b : coq_type N T) :
   do l <- cycle T a b; do l1 <- rtl l; rtl l1 = cycle T a b.
@@ -147,11 +148,6 @@ under eq_bind => r1.
   rewrite cnewget.
   over.
 rewrite cnewchk.
-(*
-under eq_bind do under eq_bind => v do rewrite -(bindretf (Cons true v)) bindA.
-under eq_bind do rewrite -bindA.
-done.
-*)
 under [RHS]eq_bind do (rewrite bindA; under eq_bind do rewrite bindretf).
 done.
 Qed.