From 41adeb51c29e0a100d318f2e01eebf3752c86658 Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Fri, 5 Jul 2024 14:07:23 +0900 Subject: [PATCH] ::: for Cons in proofs (#133) --- example_typed_store.v | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/example_typed_store.v b/example_typed_store.v index ad91c0a..266aeb4 100644 --- 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.