[Agda] One more time about Backus-Naur form

[Guillaume Brunerie]

You can use something like the following:

data T : Set where
  c1 : T1 -> T
  c2 : T2 -> T
  c3 : T3 -> T

You can then construct elements of type T by using either c1 t1 (with
t1 of type T1), c2 t2 or c3 t3, and you can define functions out of T
by pattern matching.

On 2016-03-03 13:10 GMT+01:00  <shuhray15 at yahoo.com> wrote:
> Hi
> I have a definition of the form
> T::= T_1 | T_2 | T_3
> I can use T_1+T_2+T_3 with explicit  inl, inr but it isn't a good solution.
> What can I do else?
>
> Pavel
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>