20 Sep
2006
20 Sep
'06
5:48 a.m.
On Tue, Sep 19, 2006 at 08:06:07PM +0200, apfelmus@quantentunnel.de wrote:
For our optimization problem, it's only a matter of constructors on the right hand side. They should pop out before do not look on any arguments, so it's safe to cry "so you just know, i'm a Just".
It seems the appropriate encoding would be for the shape to be an inductive datatype and the contents (as well as the lists) to be coinductive, as access to the contents is gated through the shape.