[Agda] missing record field

Serge D. Mechveliani mechvel at botik.ru
Sat Jan 12 18:38:17 CET 2013

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:

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 ...".



More information about the Agda mailing list