docs: update README

Author: favonia

README.markdown

@@ -1,12 +1,26 @@
 # 🦠 algaett’s not algaeff
 
 This development is an experiment with the following goals:
+
 1. Adopt smalltt and related techniques into the cubical world.
 2. Show how various OCaml packages of ours fit together.
 3. Write natural grammars without neccesarily conforming to LR(k).
 4. Use lots of Unicode emojis.
 
-## Smalltt
+## Try It Out!
+
+```bash
+opam pin git+https://github.com/RedPRL/bantorra
+opam pin git+https://github.com/RedPRL/algaett
+cat tests/example.ag
+algaett tests/example.ag
+```
+
+The last line should not have an output, which means it type checks!
+
+## Important Ideas
+
+### Ideas from Smalltt
 
 The core NbE algorithm closely follows [András Kovács’s smalltt.](https://github.com/AndrasKovacs/smalltt)
 Here are some notable differences:
@@ -20,16 +34,16 @@ Here are some notable differences:
    The type inference from the universe 🌌 will fail, and then the type checking will be redone with 😄 unfolded to 🌌 🆙 1️⃣.
 3. The conversion checker is generalized to handle subtyping generated by cumulativity.
 
-## Our OCaml packages
+### Modular Development
 
 - [algaeff](https://redprl.org/algaeff/algaeff/Algaeff): reusable effects-based components
-- [asai](https://redprl.org/asai/asai/Asai): error messages _(not used yet)_
-- [bantorra](https://redprl.org/bantorra/bantorra): unit resolution _(not used yet)_
+- [asai](https://redprl.org/asai/asai/Asai): error messages _(not actively used yet)_
+- [bantorra](https://redprl.org/bantorra/bantorra): unit resolution _(not actively used yet)_
 - [bwd](https://redprl.org/bwd/bwd/Bwd): backward lists
 - [mugen](https://redprl.org/mugen/mugen/Mugen): universe levels
 - [yuujinchou](https://redprl.org/yuujinchou/yuujinchou): namespaces and name modifier
 
-## Beyong LR
+### Parser beyond LR
 
 We are using the Earley’s parsing algorithm which can handle all context-free grammars.
 

test/example.ag

@@ -0,0 +1,2 @@
+📌 😄 : 🌌 🆙 2️⃣ 👉 🌌 🆙 1️⃣
+📌 _ 👉 🌌 : 😄