more doc

Author: gares

apps/derive/README.md

@@ -565,3 +565,30 @@ Elpi Typecheck derive.
 ```
 
 So when the user `Import`s `better_std` he gets a fully loaded `derive`.
+
+The code of the derivation must be put in a namespace. So `myder.elpi` should
+look like so
+
+```elpi
+namespace derive.myder {
+
+pred main i:gref, i:string, o:list prop.
+main GR Prefix Clauses :- std.do! [
+  ... % synthesize Body and Type
+  Name is Prefix ^ "myconcept",
+  coq.ensure-fresh-global-id Name FName,
+  coq.env.add-const FName Body Type _ C,
+  Clauses = [myder-done GR, myder GR (const C)],
+  std.forall Clauses (x\
+    coq.elpi.accumulate _ "derive.myder.db" (clause _ _ x)
+  ),
+].
+
+}
+```
+
+It is important that all clauses added to the database are also returned
+(see the last argument of `main`). Derive runs all derivations at once
+and databases are updated only when the program ends. So derive will
+assume, with `=>`, the clauses generated by one derivation before running the
+nest one.