From: Auke Booij <auke@tulcod.com>
Date: Thu, 2 Jun 2016 22:47:41 +0000 (+0100)
Subject: Add warning about recursive HITs
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=58c2fe92dbbb19225d7fabe4559a4e1b7a97d699;p=cubicaltt.git

Add warning about recursive HITs
---

diff --git a/examples/propTrunc.ctt b/examples/propTrunc.ctt
index 6ba72eb..146c165 100644
--- 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]