From c15dd4af9171bda720c5847b1660eb67ef6c7971 Mon Sep 17 00:00:00 2001 From: Kaiyu Yang Date: Wed, 6 Dec 2023 14:38:17 -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 f73833d..d753d0e 100644 --- a/README.md +++ b/README.md @@ -28,7 +28,7 @@ require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "v [Here](https://github.com/yangky11/lean4-example/blob/LeanCopilot-demo) is an example of a Lean package depending on Lean Copilot. If you have problems building the project, our [Dockerfile](./Dockerfile), [build.sh](scripts/build.sh) or [build_example.sh](scripts/build_example.sh) may be helpful. -### Using LeanCopilot +### Getting Started with Lean Copilot #### Tactic Suggestions