I might be not clear enough.<br>Could you please refer to this (<a href="https://github.com/dima-starosud/Uniqueness-typing-in-Agda/blob/master/HandleAPITest.agda" target="_blank">https://github.com/dima-starosud/Uniqueness-typing-in-Agda/blob/master/HandleAPITest.agda</a>).<br>
I want to get rid of:<br><pre>⇒⟦ refl ⟧⇒</pre>e.g. replace it with "then", which would mean semicolon just like in imperative program<br><br>Best regards,<br>Dmytro <br><br><div class="gmail_quote">2013/2/1 Dmytro Starosud <span dir="ltr"><<a href="mailto:d.starosud@gmail.com" target="_blank">d.starosud@gmail.com</a>></span><br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">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 "f refl", because A and B is known at compile time and if "op A ≡ op B" is inhabited then "refl" is enough, I mean I don't need to write complex proof.<br>
But "op B : Set" is undecidable, so I cannot make that proof implicit, and also I cannot make it inferable (Agda not always wants to infer "refl" even if "op A" is exactly the same as "op B").<br>
<br>Is there any way to substitute "f refl" with some "g"? I mean something like C-style macros:<br>#define g (f refl)<br><br>Thanks in advance,<br>Dmytro <br>
</blockquote></div><br>