[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