mechvel

Thank you for explanation. For understanding it is needed an example. Say, consider ``` postulate makeList : List ℕ P : Pred (List ℕ) _ P? : Decidable P f...

> ... except that, apparently for reasons we don't yet quite understand, such definitions don't quite work wrt the > typechecker in the subsequent proofs of properties, as your tests...

But my discourse above is erroneous. The requirement needs to be not only preserving the type of `f` but also (II) : preserving its data map. For example, changing the...

With lib-2.0 it worked , for example, ``filter-accept nonzeroMon? a≉0``. And lib-2.1-rc1 requires ``filter-accept nonzeroMon? {mon}{mons +ms mons'} a≉0``. I believe you can test this by considering simple examples with...

> This is a real problem that we would like to fix. Please can you provide a minimal example that type > checks in isolation only relying on Standard library...

I do not understand the details you are talking of. But I find now that the function `filter` has a bit different implementation in lib-2.0 and in lib-2.1-rc1. So, I...

This latter ``search`` version is usable and more generic than ``find``, and its implementation needs a wise additional combination of ``any, fromDec, map₁``. So that it probably worth to add...

Concerning the essence of the subject (which I do not recall/understand now) , let the team decide, and then I would decide how to apply this. My deal is mainly...

I somehow exaggerated this (a new word for me). At least this latter fragment of > and client-side post-processing (as above) can fix up the types to deliver whatever a...

``Any._-_`` is good. But the above ``delete`` is not given ``Any P xs``, so that ``delete p? xs`` sometimes returns ``xs``. May be ``delete`` is worth adding, I do not...