* Am 11.05.06 schrieb Edwin Brady:
> If, on the other hand, we do care whether it is total, we could
> implement it via the following view (sorry about the layout):
>
> ( i, j, k : Nat !
> data !----------------!
> ! Yong i j k : * )
Hi Edwin,
could you then share a quick view for the majority of us, please? Cause
i'm living without a running epigram system these days :(
> [Thinks: since the indices are non-overlapping, is it possible to
> automatically derive the covering function for views like this? I
> know it's not possible in general, but this seems to be not much more
> than an Augustsson style pattern matching compiler, and writing it
I know i'm getting repetitive on this, but there exist pattern matching
compiler implementations which care a big deal about the overlapping of
a programs indices by classifying programs as containing
inductive positions: an argument position which is instantiated with
constructors in all defining equations
demanded positions: an argument position which is instantiated with
a constructor in at least one defining equation
This is done to benefit a similar 'matter patching' of variables with
constructors too, albeit at runtime not during elaboration.
I'm still keen to know what epigram will say when fed programs like
majority in /batch mode/.
Best regards,
Sebastian
