[ fix ] derive instances for new reflection types

stefan-hoeck · Jun 8, 2021 · 731ee24 · 731ee24
1 parent 57c0910
commit 731ee24
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 15 deletions.
diff --git a/README.md b/README.md
@@ -27,4 +27,4 @@ packages useful to automatically derive interface implementations.
 For the time being, this library tries to (and is forced to) follow closely the
 latest builds of [Idris2](https://github.com/idris-lang/Idris2).
 
-The latest commit has been built against Idris 2, version 0.3.0-50d75cc3a.
+The latest commit has been built against Idris 2, version 0.3.0-aa94dd235.
diff --git a/src/Doc/Generic4.md b/src/Doc/Generic4.md
@@ -202,20 +202,23 @@ Finally, lets put our new utilities to work. Below, we derive
 from `Language.Reflection.TT` and `Language.Reflection.TTImp`.
 
 ```idris
-%runElab (derive "FC"         [Generic', Eq', Ord'])
-%runElab (derive "NameType"   [Generic', Eq', Ord'])
-%runElab (derive "Constant"   [Generic', Eq', Ord'])
-%runElab (derive "Namespace"  [Generic', Eq', Ord'])
-%runElab (derive "Name"       [Generic', Eq', Ord'])
-%runElab (derive "Count"      [Generic', Eq', Ord'])
-%runElab (derive "LazyReason" [Generic', Eq', Ord'])
-%runElab (derive "PiInfo"     [Generic', Eq', Ord'])
-%runElab (derive "BindMode"   [Generic', Eq', Ord'])
-%runElab (derive "UseSide"    [Generic', Eq', Ord'])
-%runElab (derive "DotReason"  [Generic', Eq', Ord'])
-%runElab (derive "Visibility" [Generic', Eq', Ord'])
-%runElab (derive "TotalReq"   [Generic', Eq', Ord'])
-%runElab (derive "DataOpt"    [Generic', Eq', Ord'])
+%runElab (derive "ModuleIdent"  [Generic', Eq', Ord'])
+%runElab (derive "VirtualIdent" [Generic', Eq', Ord'])
+%runElab (derive "OriginDesc"  [Generic', Eq', Ord'])
+%runElab (derive "FC"          [Generic', Eq', Ord'])
+%runElab (derive "NameType"    [Generic', Eq', Ord'])
+%runElab (derive "Constant"    [Generic', Eq', Ord'])
+%runElab (derive "Namespace"   [Generic', Eq', Ord'])
+%runElab (derive "Name"        [Generic', Eq', Ord'])
+%runElab (derive "Count"       [Generic', Eq', Ord'])
+%runElab (derive "LazyReason"  [Generic', Eq', Ord'])
+%runElab (derive "PiInfo"      [Generic', Eq', Ord'])
+%runElab (derive "BindMode"    [Generic', Eq', Ord'])
+%runElab (derive "UseSide"     [Generic', Eq', Ord'])
+%runElab (derive "DotReason"   [Generic', Eq', Ord'])
+%runElab (derive "Visibility"  [Generic', Eq', Ord'])
+%runElab (derive "TotalReq"    [Generic', Eq', Ord'])
+%runElab (derive "DataOpt"     [Generic', Eq', Ord'])
 ```
 
 ~~It seems not yet to be possible, to use this method in a mutual