[Agda] a strange "unsolved" report
James Wood
james.wood.100 at strath.ac.uk
Sun Oct 4 22:30:39 CEST 2020
Hi Sergei,
Quick questions first: is `_∷_` overloaded at all in this context?
That'd be my guess for why Agda has no clue what the type is supposed to be.
Regards,
James
On 04/10/2020 18:19, mechvel at scico.botik.ru wrote:
> Dear Agda developers,
>
> There is a question about the following code fragment:
>
> -----------------------------------------------------
> +ms-assoc-aux {monᶜ a e ∷ mons} {monᶜ b e' ∷ mons'} {monᶜ c e'' ∷
> mons''} ... =
>
> aux (<-cmp e e') (<-cmp e' e'') (<-cmp e e'')
> where
> m = monᶜ a e; m' = monᶜ b e'; m'' = monᶜ c e''
>
> mmons = m ∷ mons -- *
>
> -- m'mons' : List Mon -- (I-s)
> m'mons' = m' ∷ mons' -- (I)
>
> m''mons'' = m'' ∷ mons''
> ...
> -----------------------------------------------------
>
> Agda 2.6.1 reports
> "
> Sort _1156 [ at ...Over-abelianGroup.agda:414,5-12 ]
> _1157 : _1156 [ at ...Over-abelianGroup.agda:414,5-12 ]
> _1159 : _1157 [ at ...Over-abelianGroup.agda:414,15-25 ]
> "
>
> I guess this is the kind of "unsolved metas".
> And the first "unsolved" is about the line marked (I).
>
> The previous line (marked *) is solved - while it is not any more clear
> than (I).
>
> Then, after adding the signature (I-s), everything is type-checked.
> 1) This necessity to add signature in the middle of an array of short
> assignments of the same
> type looks strange.
> 2) There are many similar fragments in the program, and I never observed
> such an effect.
>
> What might this mean?
>
> --
> SM
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
More information about the Agda
mailing list