diff options
| author | Antonio Nikishaev | 2020-04-05 02:54:23 +0400 |
|---|---|---|
| committer | Antonio Nikishaev | 2020-04-08 01:13:13 +0400 |
| commit | 815d3cbfa2bf98b4b8f2bcd14819a20eca843e78 (patch) | |
| tree | d3564d7ccb62b38493fde1a0fc23ff94410074ec /mathcomp/ssreflect/eqtype.v | |
| parent | 14e28e78155e3e6cfbe78aee0964569283f04d7d (diff) | |
fix typos in documentation: text
Diffstat (limited to 'mathcomp/ssreflect/eqtype.v')
| -rw-r--r-- | mathcomp/ssreflect/eqtype.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index f5d95e8..296f85e 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -38,7 +38,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool. (* x != y :> T <=> x and y compare unequal at type T. *) (* x =P y :: a proof of reflect (x = y) (x == y); x =P y coerces *) (* to x == y -> x = y. *) -(* eq_op == the boolean relation behing the == notation. *) +(* eq_op == the boolean relation behind the == notation. *) (* pred1 a == the singleton predicate [pred x | x == a]. *) (* pred2, pred3, pred4 == pair, triple, quad predicates. *) (* predC1 a == [pred x | x != a]. *) @@ -73,7 +73,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool. (* insub x = Some u with val u = x if P x, *) (* None if ~~ P x *) (* The insubP lemma encapsulates this dichotomy. *) -(* P should be infered from the expected return type. *) +(* P should be inferred from the expected return type. *) (* innew x == total (non-option) variant of insub when P = predT. *) (* {? x | P} == option {x | P} (syntax for casting insub x). *) (* insubd u0 x == the generic projection with default value u0. *) @@ -92,7 +92,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool. (* [subType for S_val by Srect], [newType for S_val by Srect] *) (* variants of the above where the eliminator is explicitly provided. *) (* Here S no longer needs to be syntactically identical to {x | P x} or *) -(* wrapped T, but it must have a derived constructor S_Sub statisfying an *) +(* wrapped T, but it must have a derived constructor S_Sub satisfying an *) (* eliminator Srect identical to the one the Coq Inductive command would *) (* have generated, and S_val (S_Sub x Px) (resp. S_val (S_sub x) for the *) (* newType form) must be convertible to x. *) |