Does Agda or any other proofchecker support Backus–Naur Form? For example Nat::= Even | OddEven::= 0 | Plus2(Even)Odd::= 1 | Plus2(Odd) -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.chalmers.se/pipermail/agda/attachments/20160302/9cf2786d/attachment.html