<html><body><div style="color:#000; background-color:#fff; font-family:arial, helvetica, sans-serif;font-size:10pt"><div>Is it possible to use -> and let in syntax definitions? I've tried but I get a parse error and I'm not sure what the problem actually is. What I was thinking of was cases like this (which could be used for pattern matching in type sigs):</div><div><br></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; ">syntax (x : A) -> (let P = x in B) = [ P \: A ]-> B</div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><br></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; ">which would eliminate the need for an OPTION. similarly, you could have
sigmas that bring witnesses into scope:</div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><br></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; ">syntax (p : Sigma A B) -> (let a = proj1 p in C) = Sigma'[ a \: A ] B --> C</div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><br></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; ">- Darryl</div> </div></body></html>