Agda in Agda [Was: [Agda] Pie in the sky]

[Nils Anders Danielsson]

On 2010-09-25 12:52, Samuel Gélineau wrote:
> But given these functions, the following counter-example can be constructed:
>
> p : Bool
> p with termination-checks? (quote p)
> p | (no _) = ff  -- never reached
> p | (yes t) with eval p t
> p | (yes t) | r with syntactically-equal? r (quote tt)
> p | (yes t) | r | (yes _) = ff
> p | (yes t) | r | (no _) = tt
>
>
> Since termination-checks?, eval and syntactically-equal? are all
> assumed to pass the termination checker, the current Agda termination
> checker would also accept p as terminating.

No, the uses of p on the right-hand side are neither guarded nor applied
to structurally smaller arguments.

--
/NAD