<div dir="ltr"><div>This is a nice trick. I am concerned about two things though. We cannot use this technique selectively to specific functions, because we do not know a priori whether we will create a function like 'run'.<br></div>Doing this for all functions that use '⊥-elim' might be possible if it didn't make the code difficult to read/ didn't take too much time to implement.<br><div><div><br>My <a href="https://github.com/xekoukou/sparrow/blob/master/agda/LinFunContruct.agda#L56" target="_blank">function</a> has 21 cases with '⊥-elim' and many other cases. <br><br></div><div>I could create a 'view' type of the input that does not result into '⊥-elim', and then perform your trick. That would work.I am still unsure whether it is worth it.<br></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Jul 19, 2017 at 6:23 PM, Guillermo Calderon <span dir="ltr"><<a href="mailto:calderon@fing.edu.uy" target="_blank">calderon@fing.edu.uy</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
Hi,<br>
<br>
You can define a higher order function like this:<br>
<br>
```<br>
from-a1 :  ∀{S : (a : A)→ B a → Set}<br>
      → (B a1 → S a1 b1)<br>
      → (a : A) → (b : B a) → S a b<br>
from-a1 f a1 b1 = f b1<br>
from-a1 _ a2 b  = ⊥-elim (fun b)<br>
```<br>
<br>
Then,  you define run and gun this way:<br>
<br>
```<span class=""><br>
gun : (a : A) → (b : B a) → C b<br></span>
gun = from-a1 λ _ → c<span class=""><br>
<br>
run : (a : A) → (b : B a) → gun a b ≡ c<br></span>
run = from-a1 λ _ → refl<br>
```<br>
<br>
By the way,  for this minimal example, there is a better solution:<span class=""><br>
<br>
  run : (a : A) → (b : B a) → gun a b ≡ c<br></span>
  run .a1 b1 = refl<br>
<br>
----------<br>
Guillermo<div><div class="h5"><br>
<br>
<br>
On 18/07/17 02:10, Apostolis Xekoukoulotakis wrote:<br>
</div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5">
Consider this example :<br>
<br>
```<br>
module test where<br>
<br>
open import Data.Empty<br>
open import Relation.Binary.PropositionalE<wbr>quality<br>
open import Relation.Nullary<br>
<br>
<br>
data A : Set where<br>
   a1 a2 : A<br>
<br>
data B : A → Set where<br>
   b1 : B a1<br>
<br>
data C : ∀{a} → B a → Set where<br>
   c : ∀{a} → {b : B a} → C b<br>
<br>
fun : ¬ (B a2)<br>
fun ()<br>
<br>
<br>
gun : (a : A) → (b : B a) → C b<br>
gun a1 b = c<br>
gun a2 b = ⊥-elim (fun b)<br>
<br>
<br>
run : (a : A) → (b : B a) → gun a b ≡ c<br>
run a1 b = refl<br>
run a2 b = ⊥-elim (fun b)<br>
```<br>
<br>
For the run function, I have to provide the same proof that I gave in<br>
the gun function.<br>
If the proof is big, then it becomes cumbersome and it increases the<br>
complexity of the code.<br>
<br>
Is there a way to not do that?<br>
<br>
Keep in mind that in this example, we could avoid ⊥-elim, we could<br>
simply case split on b. I am referring to the cases where we cannot<br>
avoid ⊥-elim.<br>
<br>
<br></div></div>
______________________________<wbr>_________________<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" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br>
</blockquote>
<br>
<br>
______________________________<wbr>_________________<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" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
</blockquote></div><br></div>