From e5bb24e7da7ec4b27aea4d3e49b5122b55753e98 Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org> Date: Wed, 5 Apr 2017 16:41:12 +0200 Subject: [PATCH] Typos. --- theories/base_logic/upred.v | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v index eec44f42d..5beea6517 100644 --- a/theories/base_logic/upred.v +++ b/theories/base_logic/upred.v @@ -18,16 +18,17 @@ Record uPred (M : ucmraT) : Type := IProp { otherwise this condition is no longer limit preserving, and uPred does no longer form a COFE (i.e., [uPred_compl] breaks). This is because the distance and equivalence on this cofe ignores the - truth valid on invalid elements. This, in turns, is required by + truth value on invalid elements. This, in turn, is required by the fact that entailment has to ignore invalid elements, which is itself essential for proving [ownM_valid]. - We could, actually, make the following condition true even for - invalid elements: we have proved that uPred is isomorphic to a - sub-COFE of the COFE of predicates that are monotonous both with - respect to the step index and with respect to x. However, that - would essentially require changing (by making more complicated) - the model of many connectives of the logic, which we don't want. *) + We could, actually, remove this restriction and make this + condition apply even to invalid elements: we have proved that + uPred is isomorphic to a sub-COFE of the COFE of predicates that + are monotonous both with respect to the step index and with + respect to x. However, that would essentially require changing + (by making it more complicated) the model of many connectives of + the logic, which we don't want. *) uPred_closed n1 n2 x : uPred_holds n1 x → n2 ≤ n1 → ✓{n2} x → uPred_holds n2 x }. Arguments uPred_holds {_} _ _ _ : simpl never. -- GitLab