A proper way to implement CATA is given
as follows (if you want to perform terminationchecking):
primplmnt
{A}{B}
CATA{n}(F, A) = cata{n}(F, A) where
{
prfun
cata{n:nat} ..
(F: ALGEBRA(A,B), A: FUNCTOR_PROP(A,n)) : B =
sif
(n==0)
then
F(LISTF_PROP_NIL())
else
Neat, thanks! I'll update the list once I have something more substantial :)
On 08/11/2018 08:53 PM, Hongwei Xi wrote:
> I modified your first version as follows
> (based some guessing on my part). It typechecks now.
>
> absprop FUNCTOR_PROP (A : prop, n : int)
>
> absprop BASE_FUNCTOR_PROP (A :
I modified your first version as follows
(based some guessing on my part). It typechecks now.
absprop FUNCTOR_PROP (A : prop, n : int)
absprop BASE_FUNCTOR_PROP (A : prop, B : prop)
// TODO: prooflevel paramorphisms?
dataprop LIST_PROP(A: prop, int) =
 LIST_PROP_NIL(A, 0) of ()
