From c12240a8cc44a6cdf649d35b41210a59a60dfa8f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Tue, 12 Jan 2016 14:26:49 +0100
Subject: [PATCH] Destructor for cons.
---
theories/list.v | 3 +++
1 file changed, 3 insertions(+)
diff --git a/theories/list.v b/theories/list.v
index 84c0b17..6e0bac8 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -34,6 +34,9 @@ Notation "x ≢ₚ y":= (¬x ≡ₚ y) (at level 70, no associativity) : C_scope
Notation "( x ≢ₚ)" := (λ y, x ≢ₚ y) (only parsing) : C_scope.
Notation "(≢ₚ x )" := (λ y, y ≢ₚ x) (only parsing) : C_scope.
+Instance maybe_cons {A} : Maybe2 (@cons A) := λ l,
+ match l with x :: l => Some (x,l) | _ => None end.
+
(** * Definitions *)
(** Setoid equality lifted to lists *)
Inductive list_equiv `{Equiv A} : Equiv (list A) :=
--
2.26.2