<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body dir="ltr">
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
Hi,</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
please consider follow program:</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<span> foo : ℕ → Set<br>
</span>
<div> foo 0 = {!!}<br>
</div>
<div> foo a = {!!}<br>
</div>
<span></span></div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
In Emacs, the third line, `foo a`, will be highlighted. I know that I can get away with this by expanding `a` to be `suc a`. However, in my real project, this expansion corresponds to 5 cases, and their proof body are exactly the same.</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
I understand that this does not introduce any unsoundness, but I want to understand what's the reason behind this highlight, and is there any programming idiom so that I can get away with this highlight without having expand the cases here?<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div id="signature">
<div id="divtagdefaultwrapper" dir="ltr" style="font-size:12pt; color:#000000; font-family:Calibri,Arial,Helvetica,sans-serif">
<div><font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b>Sincerely Yours,<br>
</b></span></span></font></div>
<font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b><br>
Jason Hu<a target="_blank"></a></b></span></span></font> </div>
</div>
</body>
</html>