Fwd: [Agda] Parallel or

[Nils Anders Danielsson]

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 = _

-- 
/NAD