[Agda] two questions on type checker

[Guillaume Allais]

Note that you can use an @ pattern to bind x'xs like so:
lemma' y (x ∷ x'xs@(x' ∷ xs)) _

A let-binding (rather than a where) should also work

On 24/09/18 14:50, Sergei Meshveliani wrote:
> Dear Agda developers
> 
> I have two notes on a code of kind
> 
> ----------------------------------------------------
> lemma' y (x ∷ x' ∷ xs) _ i@(suc k , 1+k<|xx'xs|) =
>   begin
>     ... 
>     lookup' (x' ∷ xs) (k , k<|x'xs|)
>                     ≡⟨ lemma' y x'xs 0<|x'xs| (k , k<|x'xs|)
>     ...
>   where
>   x'xs = x' ∷ xs
>   ...
> ----------------------------------------------------
> 
> Agda 2.6.0-05e8112  reports
> 
> -----------------
> Termination checking failed for the following functions:
>   lemma'
> Problematic calls:
>   lemma' y (x'xs y x x' xs x₁ k 1+k<|xx'xs|)
>   (0<|x'xs| y x x' xs x₁ k 1+k<|xx'xs|)
>   (k , k<|x'xs| y x x' xs x₁ k 1+k<|xx'xs|)
>   ...
> ------------------
> 
> First, the print-out of the  lemma'  call in the message differs greatly
> from the source code. Blanks inserted into identifiers, `∷' skipped etc.
> 
> Second, with expanding  x'xs  to (x' ∷ xs)  in the recursive call, Agda
> sees termination.
> Many users will not guess to do this expansion and will spend effort
> trying to provide a wise termination proof.
> If it is problematic to fix the feature, may be, Agda could issue some
> hints after the message about termination - ?
> 
> Regards,
> 
> ------
> Sergei
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180924/e1b9c7d3/attachment.sig>