Fwd: [Agda] Parallel or

[Nils Anders Danielsson]

On 2011-11-21 00:27, wren ng thornton wrote:
> Ah, curious. I guess we'd have to exclude the indexing of Pi if we're
> using or-patterns. That's quite an unsavory restriction.

You could still use or-patterns to indicate which right-hand sides you
want to be equal, and then Agda can check for syntactic equality after
unification etc. However, it's not obvious what to do if there is a goal
in the RHS.

-- 
/NAD