From 4ed0eb8b3f6917f1754543c7f9fedfff8d147e28 Mon Sep 17 00:00:00 2001
From: "J. Bergmann" <bergmannj@posteo.de>
Date: Tue, 21 May 2024 14:11:14 +0200
Subject: [PATCH] docs: update readme

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

diff --git a/README.md b/README.md
index 46e8767..73adcb0 100644
--- a/README.md
+++ b/README.md
@@ -27,17 +27,35 @@ The main documentation is in [Regex.lean](https://bergmannjg.github.io/regex/Reg
 
 ## Example
 
+Get captures of "∀ (n : Nat), 0 ≤ n" :
+
+```lean
+def Main : IO Unit := do
+  let re := regex% r"^\p{Math}\s*([^,]+),\s*(\p{Nd})\s*(\p{Math})\s*([a-z])$"
+  let captures := Regex.captures "∀ (n : Nat), 0 ≤ n" re
+  IO.println s!"{captures}"
+```
+
+Output is
+
 ```lean
--- build `re` at compile time
-def re := regex% "a?b"
--- searches for the first match in `re`
-#eval Regex.captures "b" re
-
---Output is
---fullMatch: 'b', 0, 1
---groups: #[]
+fullMatch: '∀ (n : Nat), 0 ≤ n', 0, 22
+groups: #[(some ('(n : Nat)', 4, 13)), (some ('0', 15, 16)),
+          (some ('≤', 17, 20)), (some ('n', 21, 22))]
 ```
 
+Api
+
+- *regex%* : notation to build the regular expression at compile time
+- *captures* : searches for the first match of the  regular expression
+
+Components of regular expression:
+
+- *^* : Assertion Start of line
+- *\p{Math}* : match all characters with the Math property
+- *\s\** : match white space
+- *(\p{Nd})* : capturing group of numeric characters
+
 ## Test
 
 The library is tested with the [testdata](./testdata) of Rust Regex crate.