The current Label infrastructure, as used by Desc, doesn't work with IDesc.
There has been proposal for fixing (cf. model/ILabel.agda), however it doesn't
cope with naming in the proof state.
If we are to find a clean solution, I wish we could remove the concept of FAKE
ref: it introduces special cases in the source, hence increasing the
complexity. Now, I've no clue if it is feasible, it's wishful thinking.
Original issue reported on code.google.com by pedag...@gmail.com on 23 Aug 2010 at 1:20
Original issue reported on code.google.com by
pedag...@gmail.comon 23 Aug 2010 at 1:20