Yes, I tried &#39;syntax&#39;, but for me it is not obvious enough how it should be used.<br>What did you mean &quot;Default arguments or eta-expansion for the propositional equality&quot;?<br>I am newbie in this area and I may not know enough about some features.<br>
Could you point me to some related documents?<br><br>Thanks a lot,<br>Dmytro <br><br><div class="gmail_quote">2013/2/3 Andreas Abel <span dir="ltr">&lt;<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>&gt;</span><br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Well you can always use the C preprocessor, but then you are restricted to batch-mode Agda.  Which isn&#39;t what you want, I suppose.<br>

<br>
Did you try the &#39;syntax&#39; facility?   (Might not work...)<br>
<br>
Default arguments or eta-expansion for the propositional equality might help you, but these are not or not yet in Agda.<br>
<br>
Cheers,<br>
Andreas<div class="im"><br>
<br>
On 02.02.13 11:51 AM, Dmytro Starosud wrote:<br>
</div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">
I might be not clear enough.<br>
Could you please refer to this<br>
(<a href="https://github.com/dima-starosud/Uniqueness-typing-in-Agda/blob/master/HandleAPITest.agda" target="_blank">https://github.com/dima-<u></u>starosud/Uniqueness-typing-in-<u></u>Agda/blob/master/<u></u>HandleAPITest.agda</a>).<br>

I want to get rid of:<br>
<br>
⇒⟦ refl ⟧⇒<br>
<br>
e.g. replace it with &quot;then&quot;, which would mean semicolon just like in<br>
imperative program<br>
<br>
Best regards,<br>
Dmytro<br>
<br>
2013/2/1 Dmytro Starosud &lt;<a href="mailto:d.starosud@gmail.com" target="_blank">d.starosud@gmail.com</a><br></div>
&lt;mailto:<a href="mailto:d.starosud@gmail.com" target="_blank">d.starosud@gmail.com</a>&gt;&gt;<div class="im"><br>
<br>
    Hello list,<br>
<br>
    I have the following code (simplified).<br>
<br>
    A B : Set<br>
<br>
    Ty : Set → Set → Set<br>
    op : Set → Set<br>
<br>
    f : ∀ {A B} → op A ≡ op B → Ty A B → Ty B A<br>
    x : Ty A B<br>
<br>
    y = f refl x<br>
<br>
    I should always write &quot;f refl&quot;, because A and B is known at compile<br>
    time and if &quot;op A ≡ op B&quot; is inhabited then &quot;refl&quot; is enough, I mean<br>
    I don&#39;t need to write complex proof.<br>
    But &quot;op B : Set&quot; is undecidable, so I cannot make that proof<br>
    implicit, and also I cannot make it inferable (Agda not always wants<br>
    to infer &quot;refl&quot; even if &quot;op A&quot; is exactly the same as &quot;op B&quot;).<br>
<br>
    Is there any way to substitute &quot;f refl&quot; with some &quot;g&quot;? I mean<br>
    something like C-style macros:<br>
    #define g (f refl)<br>
<br>
    Thanks in advance,<br>
    Dmytro<br>
<br>
<br>
<br>
<br></div>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
<br><span class="HOEnZb"><font color="#888888">
</font></span></blockquote><span class="HOEnZb"><font color="#888888">
<br>
-- <br>
Andreas Abel  &lt;&gt;&lt;      Du bist der geliebte Mensch.<br>
<br>
Theoretical Computer Science, University of Munich<br>
Oettingenstr. 67, D-80538 Munich, GERMANY<br>
<br>
<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a><br>
</font></span></blockquote></div><br>