From 2783aea940d01ead99395589bed3ccfa87382e9b Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Tue, 2 Apr 2013 09:59:06 +0200 Subject: [PATCH] Assorted changes to permissions and assertions. --- theories/base.v | 3 +++ 1 file changed, 3 insertions(+) diff --git a/theories/base.v b/theories/base.v index 49cc37e9..88654324 100644 --- a/theories/base.v +++ b/theories/base.v @@ -684,6 +684,9 @@ Class FreshSpec A C `{ElemOf A C} }. (** * Miscellaneous *) +Class Half A := half: A → A. +Notation "x .½" := (half x) (at level 20, format "x .½") : C_scope. + Lemma proj1_sig_inj {A} (P : A → Prop) x (Px : P x) y (Py : P y) : x↾Px = y↾Py → x = y. Proof. injection 1; trivial. Qed. -- GitLab