Fwd: [Agda] Parallel or

[wren ng thornton]

On 11/17/11 9:43 AM, Nils Anders Danielsson wrote:
> On 2011-11-17 08:21, wren ng thornton wrote:
>> Alternatively, rather than trying to automatically determine the
>> equivalence of the RHS, we could enforce it syntactically / require it
>> intensionally by introducing or-patterns a la OCaml. Thus,
>>
>> or True _ || or _ True = True
>> or False False = False
>>
>> (using whatever syntax you'd prefer.)
>
> Your syntactic restriction doesn't enforce equivalence:
>
> record Unit : Set where
>
> record Unit₂ : Set where
> field u : Unit
>
> F : Bool → Set
> F true = Unit
> F false = Unit₂
>
> f : (b : Bool) → F b
> f true || f false = _


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.

-- 
Live well,
~wren