From a41ab337a862eb7f6a80c71b7645acd6a7936156 Mon Sep 17 00:00:00 2001 From: Matthieu Baty <matthieu.baty@epfl.ch> Date: Fri, 31 Mar 2023 09:42:39 +0000 Subject: [PATCH] Update README.md --- README.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 4b68f05..70bcd2b 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. -- GitLab