[Agda] Help, I'm failing at sized types.

[Jan Stolarek]

data Foo : {i : Size} -> Set where
  boo : {i : Size} -> Foo {i}
  coo : {i : Size} -> Foo {i} -> Foo {up i}

subtype? : {i : Size} -> Foo {i} -> Foo {infty}
subtype?  boo    = boo
subtype? (coo t) = subtype? t

Does that work for you?

Janek


Dnia piątek, 13 marca 2015, Conor McBride napisał:
> Hi
>
> Sorry to be a nuisance.
>
> I’m trying to do some stuff with sized types, but I think I’m failing at
> basic stuff like finding the on-switch. Specifically…
>
> ****************************************
> {-# OPTIONS --sized-types #-}
>
> module SizeFail where
>
> open import Agda.Primitive
> postulate
>   Size : Set
>   Size<_ : Size -> Set
>   up : Size -> Size
>   infty : Size
> {-# BUILTIN SIZE Size #-}
> {-# BUILTIN SIZELT Size<_ #-}
> {-# BUILTIN SIZESUC up #-}
> {-# BUILTIN SIZEINF infty #-}
>
> data Foo : Size -> Set where
>   boo : {i : Size} -> Foo i
>   coo : {i : Size} -> Foo i -> Foo (up i)
>
> subtype? : {i : Size} -> Foo i -> Foo infty
> subtype? t = t
> ****************************************
>
> …results in the complaint...
>
> .i != infty of type Size
> when checking that the expression t has type Foo infty
>
> …whether the pragmas are present or not.
>
> Any light gratefully received.
>
> (Longer term, I want to do some syntactic mangling in which renaming is
> obviously size-preserving, so I can apply a renaming to a substructure
> before I do a recursive call on it.)
>
> Cheers
>
> Conor_______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda



---
Politechnika Łódzka
Lodz University of Technology

Treść tej wiadomości zawiera informacje przeznaczone tylko dla adresata.
Jeżeli nie jesteście Państwo jej adresatem, bądź otrzymaliście ją przez pomyłkę
prosimy o powiadomienie o tym nadawcy oraz trwałe jej usunięcie.

This email contains information intended solely for the use of the individual to whom it is addressed.
If you are not the intended recipient or if you have received this message in error,
please notify the sender and delete it from your system.