Add warning about recursive HITs

diff --git a/examples/propTrunc.ctt b/examples/propTrunc.ctt
index 6ba72eb201162b25b9bdca18ebd6b3d64f774278..146c1655d76be3092f872094a39d98ce246ae070 100644 (file)
--- a/examples/propTrunc.ctt
+++ b/examples/propTrunc.ctt
@@ -2,6 +2,14 @@ module propTrunc where
 
 import prelude
 
+{-
+Warning: as of commit ff8a026, recursive HITs with parameters are not
+implemented correctly. Because of that, you may find unexpected results when
+using this module.
+
+See e.g. github issue #35 and pull request #39 for details.
+-}
+
 data pTrunc (A : U)
   = inc (a : A)
   | inh (x y : pTrunc A) <i> [(i=0) -> x, (i=1) -> y]