diff --git a/README.md b/README.md index 4b68f05a62f9b4d0b0570dd2af33f50b7d2e5361..70bcd2ba7fb3fb9b530b48913a9d8e3ac48b7416 100644 --- a/README.md +++ b/README.md @@ -18,7 +18,7 @@ second on my computer - slow enough to be noticed, but not too slow. * [`manual_check_slower_than_Qed`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/manual_check_slower_than_Qed.v) : `Qed` is more efficient at typechecking than `Definition` or `Check`. * [`memoization`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/memoization.v) - : `vm_compute` memoizes the value of constants. + : `vm_compute` memoizes constants. * [`names`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/names.v) : non-breaking spaces can be used in identifiers for some reason. * [`name_checking_halfway`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/name_checking_halfway.v) @@ -28,10 +28,10 @@ second on my computer - slow enough to be noticed, but not too slow. * [`nonlinear_computation`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/nonlinear_computation.v) : twice as much work can take more than twice as much time. * [`now_is_not_reflexivity`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/now_is_not_reflexivity.v) - : easy is slower than reflexivity, and `now` uses `easy`. + : easy tends to be slower than reflexivity, and `now` uses `easy`. * [`simpl_vs_cbn`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/simpl_vs_cbn.v) : `simpl` doesn't like deep nestings. * [`time_lies`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/time_lies.v) : take `Time`'s output with a pinch of salt. * [`unfolding_and_traces`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/unfolding_and_traces.v) - : `unfold` and `intro` don't commute! + : `unfold` and `intro` don't commute.