[Agda-dev] Positivity checker and abstract blocks

[Andrés Sicard-Ramírez]

Andreas,

On 3 January 2016 at 12:09, Andreas Abel <abela at chalmers.se> wrote:
> From what you quote, both seem to be GuardPos...

You are right, I made a mistake when I wrote my question. While
rewriting my question I realised that data type inside the abstract
block is `StrictPos` and the data type outside the abstract block is
`GuardPos`, so I have no question.

Thanks,

-- 
Andrés