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

[Benja Fallenstein]

Hi Nils,

On Sat, Sep 25, 2010 at 9:53 PM, Nils Anders Danielsson
<nad at cs.nott.ac.uk> wrote:
>> 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.

But Samuel said (quote p) should be "an informal notation for the
Program representing p," not an Agda function -- I take this to mean
(quote p) is informal notation for "an expression whose value is the
source of p," using quining. And the "eval p t" is surely a typo and
should be "eval (quote p) t".

- Benja