[Agda] hot computer churns codata

[Andrés Sicard-Ramírez]

Hi Conor,

I could type check the file disabling the termination check

$ time agda --no-termination-check MTypes.agda
Checking /tmp/MTypes.agda.

Unsolved metas at the following locations:
  /tmp/MTypes.agda:273,9-13

real	5m11.720s
user 5m8.907s
sys	0m1.856s

(Without to disable the termination check, I couldn't)

Best,


On Tue, May 19, 2009 at 3:47 PM, Conor McBride
<conor at strictlypositive.org> wrote:
> Friends
>
> I'm trying to typecheck a file and my left leg is about to burst into
> flames. I attach the file.
>
> It's an extensional universe construction with coinductive families.
> It goes wild when I try to prove that an unfold is equal to its
> unfolding (where "equal" means bisimilar, in a coinductively defined
> way). There's only the one corecursive definition in the whole piece:
>
> codata Co (T : Set) : Set where
>  [_] : T -> Co T
>
> ! : forall {T} -> Co T -> T
> ! [ t ] = t
>
> data M (I : Set)(S : I -> Set)(P : (i : I) -> S i -> Set)
>         (r : (i : I)(s : S i) -> P i s -> I)(i : I) : Set where
>  edon : (s : S i) -> ((p : P i s) -> Co (M I S P r (r i s p))) -> M I S P r
> i
>
> unfold : forall {I S P r}
>         (C : I -> Set)
>         (s : (i : I) -> C i -> S i)
>         (m : (i : I)(c : C i)(p : P i (s i c)) -> C (r i (s i c) p)) ->
>         (i : I) -> C i -> M I S P r i
> unfold C s m i c = edon (s i c) \ p -> [ unfold C s m _ (m i c p) ]
>
> Everything else gets done with unfold. Am I doing it wrong?
>
> I notice that ~ isn't special any more.
>
> Of course, maybe my computer is just puny.
>
> Confused...
>
> Conor
>
>
>
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>



-- 
Andrés