From 92ca833745b4e1bb170d214ec5bddc2b42699b7b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C5=81ukasz=20Czajka?=
 <62751+lukaszcz@users.noreply.github.com>
Date: Fri, 13 Dec 2024 10:11:38 +0100
Subject: [PATCH] Update README.md

---
 README.md | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/README.md b/README.md
index 35a11f1..65e7d9a 100644
--- a/README.md
+++ b/README.md
@@ -1,7 +1,7 @@
-# Juvix Lean formalization library
+# Juvix library for Lean 4
 
 The Juvix Lean library provides primitives for verifying the correctness of Juvix compiler runs, i.e., proving that the semantics of a particular Juvix program is preserved by the compilation process.
 
-The major components of the library include:
-- formalization of Juvix compiler internal representations and their semantics,
-- proof-producing metaprograms for verifying that individual Juvix compiler transformations preserve the semantics.
+The library includes:
+- formalization of Juvix compiler internal representations (IRs) and their semantics,
+- proof-producing metaprograms for verifying that Juvix compiler transformations preserve the semantics of concrete IR programs.