[Agda] missing record field

[James Chapman]

I think you have a good point.

Please add it as a feature request on the bug tracker. This is the
best place for such comments I think.

Regards,

James

On Sat, Jan 12, 2013 at 7:38 PM, Serge D. Mechveliani <mechvel at botik.ru> wrote:
> Dear Agda developers,
>
> Forgetting to implement a field in a record leads to a report of
> "Unsolved metas"
> (in  Agda-2.3.2 - MAlonzo).
> For example,
>   record Foo : Set  where field foo1 : Bool
>                                 foo2 : Bool
>                                 foo3 : Bool
>   rec = record{ foo1 = true                  -- line No 14
>               ; foo3 = true }
>
> yields the report
> "Unsolved metas at the following locations:
>   /home/mechvel/doconA/0.01/reports/3/Main.agda:14,7-17,14
>
> In a similar situation, I thought a long of what is wrong about  _+p_
> in  record { foo1 = _+p_;
>              ...
>            }
> Finally it has occured that one of the further fields has been skipped.
>
> It will be more helpful to report of
> "Missing implementation for the field  foo2 ...".
>
> Regards,
>
> ------
> Sergei
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda