From a053ad9739248ade939aa04355672362221883d7 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 18 Sep 2023 13:58:52 +0200
Subject: Update the README

---
 README.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/README.md b/README.md
index 31dc74f4..768c4277 100644
--- a/README.md
+++ b/README.md
@@ -105,6 +105,8 @@ support for partial functions and extrinsic proofs of termination (see
 and tactics specialized for monadic programs (see
 `./backends/lean/Base/Progress/Progress.lean` and `./backends/hol4/primitivesLib.sml`).
 
+A tutorial for the Lean backend is available [here](./tests/lean/Tutorial.lean).
+
 ## Formalization
 
 The translation has been formalized and published at ICFP2022: [Aeneas: Rust
-- 
cgit v1.2.3