[Agda] nontermination and Sized types

[James Wood]

My experience, as an occasional user of this stuff, is that `Size<` is
broken, and you have to make do with `↑`, `_⊔_`, &c. This makes it a
really bad thing that the example in the documentation uses `Size<` (if
my impressions are correct).

James

On 03/10/2020 08:33, vlad wrote:
> Thank you very much for the information. IMO this bug and others
> (incompatibility of sized types with equality, ...) should be better
> documented.
> 
> Best regards,
> 
>  - Vlad
> 
> On 02/10/2020 15:52, Andrew M. Pitts wrote:
>>> On 2 Oct 2020, at 13:36, vlad <Vlad.Rusu at inria.fr> wrote:
>>>
>>> Looking at (V2) one can notice that nonterminating'  looks like a
>>> well-founded induction principle for the _<_ relation on Size,
>>> defined by j < i iff (t : Size< i). Which is strange since _<_ is
>>> *not* well founded, as ∞ < ∞ holds. Indeed, if nonterminating' were
>>> accepted then it could be used to prove that _<_ is  well  founded:
>>> just take P s = "there is no infinite <-decreasing sequance starting
>>> at s". So, I believe the Agda termination checker rightfully rejects
>>> the definition (V2).
>> I believe issue #3026 is still open and that at the moment (v2.6.1)
>> Agda allows one to prove _<_ for Size is well-founded and hence derive
>> a logical inconsistency. :-)
>>
>> Andy
>>
>>
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>