Import everything from README.agda (including tests)

README.agda

@@ -0,0 +1,18 @@
+{-# OPTIONS --rewriting #-}
+
+import Generics.Prelude
+import Generics.Telescope
+
+import Generics.Desc
+import Generics.HasDesc
+import Generics.Reflection
+
+import Generics.Constructions.Case
+import Generics.Constructions.DecEq
+import Generics.Constructions.Elim
+import Generics.Constructions.Induction
+import Generics.Constructions.NoConfusion
+import Generics.Constructions.Show
+
+-- Examples
+import Parametrized

examples/Parametrized.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --rewriting #-}
+{-# OPTIONS --rewriting --allow-unsolved-metas #-}
 open import Generics.Prelude hiding (lookup)
 open import Generics.HasDesc
 open import Generics.Reflection
@@ -101,7 +101,7 @@ module Id where
   idHasDesc = badconvert (testing Id)
 
   postulate P : {A : Set} {x y : A} → Id A x y → Set
-  
+
   -- t : ∀ {A} {x y : A} (p : Id A x y) → P p
   -- t = elim″ idHasDesc P {!!}
 
@@ -114,5 +114,5 @@ module Test {ℓ} where
 
   maybeHasDesc : HasDesc (Maybe {ℓ})
   maybeHasDesc = badconvert (testing Maybe)
-  
+
 -}

tests.agda-lib

@@ -0,0 +1 @@
+include: examples