Skip to content

Copatterns desugaring bug #28

@sualitu

Description

@sualitu

Given a tree:

corecord Tree : Type -> Type where
  value : Tree a -> a
  left  : Tree a -> Tree a
  right : Tree a -> Tree a

The following two should be equivalent:

total causal grow : (Nat, Nat) -> Tree(Nat, Nat)
grow (n, d) = MkTree (n, d) (grow (n, n + d)) (grow (n + d, d))

total causal grow' : (Nat, Nat) -> Tree (Nat, Nat)
&value grow' (n, d) = (n, d)
&left  grow' (n, d) = grow' (n, n + d)
&right grow' (n, d) = grow' (n + d, d)

The one without copatterns work, however the one with copatterns give the following error:

simple.idr:69:14:No type declaration for value

Either I am missing something or this is a bug.

Metadata

Metadata

Assignees

No one assigned

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions