[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:
  /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


More information about the Agda mailing list