From: Auke Booij 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=0) -> x, (i=1) -> y]