[Agda] missing record field

[Dan Licata]

It's nice that when a field is missing and it *is* inferable, Agda
doesn't complain about the missing field, though.  I've seen this used
for infering proof obligations with no visual trace, when the type
reduces Unit or something like that.

-Dan

On Jan13, James Chapman wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda