search

UlfNorell / agda-test

Agda test
0 stars 0 forks source link

Can't give COMPILED_DATA pragma for mutually recursive data #223

Open UlfNorell opened 10 years ago

UlfNorell commented 10 years ago

From darinmor...@gmail.com on November 09, 2009 16:15:07

Given the following code, it appears impossible to give COMPILED_DATA pragmas for Neu or Nrm:

mutual data Neu : Set where var : Var → Neu · : Neu → Nrm → Neu tt : Neu ∶ : Nrm → Type → Neu

data Nrm : Set where ƛ_ : Nrm → Nrm neu : Neu → Nrm

If you try to give a COMPILED_DATA pragma for Neu first, it will complain that it does not know how to translate Nrm to a Haskell type. If you give the COMPILED_DATA pragma for Nrm first, it will complain that it does not know how to translate Neu to a Haskell type.

Original issue: http://code.google.com/p/agda/issues/detail?id=223

UlfNorell commented 10 years ago

From ulf.nor...@gmail.com on November 18, 2009 02:27:16

Status: Accepted
Labels: Type-Defect Priority-Medium

UlfNorell commented 10 years ago

From ulf.nor...@gmail.com on November 18, 2009 02:27:31

Owner: ulf.norell

UlfNorell commented 10 years ago

From nils.anders.danielsson on September 02, 2011 12:57:02

Issue 419 has been merged into this issue.

Cc: ulf.nor...@gmail.com