From 7416bac27ce582e1270ca155b6343cbb2d03912e Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Tue, 12 Nov 2024 03:29:01 -0500 Subject: [PATCH] chore: update readme --- README.md | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index ce000cb2..5ff9962f 100644 --- a/README.md +++ b/README.md @@ -34,11 +34,18 @@ Add the following dependency to your project's `lakefile.toml`: ```toml [[require]] -name = "lean4-unicode-basic" +name = "UnicodeBasic" git = "https://github.com/fgdorais/lean4-unicode-basic.git" rev = "main" # or any specific revision ``` +Or this dependency to your project's `lakefile.lean`: + +```lean4 +require UnicodeBasic from git + "https://github.com/fgdorais/lean4-unicode-basic.git" @ "main" +``` + Then add `import UnicodeBasic` at the top of any Lean file where you plan to use this library. ## Usage