
<html><head></head><body><div style="color:#000; background-color:#fff; font-family:HelveticaNeue, Helvetica Neue, Helvetica, Arial, Lucida Grande, sans-serif;font-size:16px"><div dir="ltr" id="yui_3_16_0_1_1456945978867_3646">Does Agda or any other proofchecker support <span id="yui_3_16_0_1_1456945978867_3767" class="st"> Backus–Naur Form? For example</span></div><div id="yui_3_16_0_1_1456945978867_3752" dir="ltr"><br><span class="st"></span></div><div id="yui_3_16_0_1_1456945978867_3789" dir="ltr"><span class="st">Nat::= Even | Odd</span></div><div id="yui_3_16_0_1_1456945978867_3768" dir="ltr"><span class="st">Even::= 0 | Plus2(Even)</span></div><div id="yui_3_16_0_1_1456945978867_3751" dir="ltr"><span class="st">Odd::= 1 | Plus2(Odd)<br></span></div></div></body></html>