From a70ec42dd507f6800c7f871a0da45d6b9eda02ea Mon Sep 17 00:00:00 2001 From: Dan Frumin <dan@groupoid.moe> Date: Thu, 20 May 2021 18:01:00 +0200 Subject: [PATCH] doc comment --- theories/typing/types.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/theories/typing/types.v b/theories/typing/types.v index 678eb6c..00d84e0 100644 --- a/theories/typing/types.v +++ b/theories/typing/types.v @@ -250,14 +250,14 @@ Proof. destruct op; naive_solver. Qed. (***********************************) (** Closedness of typed programs *) -(* DF: It is not trivial to prove the closedness lemma for -[is_closed_expr], because it requires a lemma like this: +(* DF: It is not trivial to prove the closedness theorem by using the +definition of [is_closed_expr] as it is, because it would require (for +one of the cases) a lemma like this: - Lemma elements_insert Γ x τ : - elements (dom stringset (<[x:=τ]> Γ)) = x :: elements (dom stringset Γ). + elements (dom (<[x:=τ]> Γ)) = x :: elements (dom Γ). -But this does not hold (it holds only up to multiset equality). -So we use an auxiliary definition with sets *) +But this does not hold (it holds only up to multiset equality). So we +use an auxiliary definition with sets *) Definition maybe_insert_binder (x : binder) (X : stringset) : stringset := match x with -- GitLab