[Agda] Re: Backus-Naur form

[Sergei Meshveliani]

shuhray15 at yahoo.com  wrote

> Does Agda or any other proofchecker support  Backus–Naur Form? For
> example
> Nat::= Even | OddEven::= 0 | Plus2(Even)Odd::= 1 | Plus2(Odd)


May be this is by the `data' construct?
For example,

  data Even : ℕ → Set 
       where  
       even0  : Even 0
       even+2 : {n : ℕ} → Even n → Even (suc (suc n))

Regards,

------
Sergei