chore(docs/user): produce a simple Factorial example

I extracted a Factorial example in Rust to Lean.

Signed-off-by: Ryan Lahfa <[email protected]>

Author: Ryan Lahfa

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

docs/user/src/lean/basics/factorial.lean.md

@@ -0,0 +1 @@
+{{#include factorial.lean}}