From e340a843db034333c6c4c2ccaa836e21bdb8cbab Mon Sep 17 00:00:00 2001
From: Ryan Lahfa <ryan.lahfa@inria.fr>
Date: Tue, 20 Aug 2024 17:43:47 +0200
Subject: [PATCH] chore(docs/user): produce a simple Factorial example

I extracted a Factorial example in Rust to Lean.

Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
---
 docs/user/src/lean/basics/factorial.lean    | 26 +++++++++++++++++++++
 docs/user/src/lean/basics/factorial.lean.md |  1 +
 2 files changed, 27 insertions(+)
 create mode 100644 docs/user/src/lean/basics/factorial.lean
 create mode 100644 docs/user/src/lean/basics/factorial.lean.md

diff --git a/docs/user/src/lean/basics/factorial.lean b/docs/user/src/lean/basics/factorial.lean
new file mode 100644
index 000000000..86e31fbaa
--- /dev/null
+++ b/docs/user/src/lean/basics/factorial.lean
@@ -0,0 +1,26 @@
+import Base
+
+/-!
+
+# Computing factorial
+
+-/
+
+open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+namespace factorial
+
+/- [factorial::factorial]:
+   Source: 'src/factorial.rs', lines 1:0-1:27 -/
+divergent def factorial (n : U64) : Result U64 :=
+  if n = 0#u64
+  then Result.ok 1#u64
+  else do
+       let i ← n - 1#u64
+       let i1 ← factorial i
+       n * i1
+
+end factorial
diff --git a/docs/user/src/lean/basics/factorial.lean.md b/docs/user/src/lean/basics/factorial.lean.md
new file mode 100644
index 000000000..8a91f2f2d
--- /dev/null
+++ b/docs/user/src/lean/basics/factorial.lean.md
@@ -0,0 +1 @@
+{{#include factorial.lean}}