From c834522dcc97e84af356adaa53b0abcdac39ded7 Mon Sep 17 00:00:00 2001 From: Kaiyu Yang Date: Sun, 10 Dec 2023 12:48:03 -0800 Subject: [PATCH] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 829f022..470e179 100644 --- a/README.md +++ b/README.md @@ -136,7 +136,7 @@ In principle, it is possible to run any model using Lean Copilot through `Extern ## Caveats -* Lean may occasionally crash when restarting or editing a file. Restarting the file again should fix the problem +* Lean may occasionally crash when restarting or editing a file. Restarting the file again should fix the problem. * `select_premises` always retrieves the original form of a premise. For example, `Nat.add_left_comm` is a result of the theorem below. In this case, `select_premises` retrieves `Nat.mul_left_comm` instead of `Nat.add_left_comm`. ```lean @[to_additive]