<div dir="ltr"><div>Hi Wouter,</div><div><br></div><div>I think your best bet here is using reflection. Something like</div><div><br></div><div style="margin-left:40px"><span style="font-family:monospace">open import Agda.Builtin.Bool<br>open import Agda.Builtin.Equality<br>open import Agda.Builtin.Reflection<br>open import Agda.Builtin.Unit<br>open import Agda.Builtin.List<br><br>id : Bool → Bool<br>id false = false<br>id true  = true<br><br>the-hammer : Term → TC ⊤<br>the-hammer hole = unify hole (con (quote refl) [])<br><br>smash-bool : (tac : Term → TC ⊤) {P : Bool → Set}<br>             {@(tactic tac) f : P false}<br>             {@(tactic tac) t : P true} →<br>             ∀ b → P b<br>smash-bool tac {f = f} {t = t} false = f<br>smash-bool tac {f = f} {t = t} true  = t<br><br>id-id : ∀ b → id b ≡ b<br>id-id = smash-bool the-hammer</span></div><div><br></div><div>/ Ulf<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Jun 3, 2021 at 11:04 AM Swierstra, W.S. (Wouter) <<a href="mailto:W.S.Swierstra@uu.nl">W.S.Swierstra@uu.nl</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Dear all,<br>
<br>
Suppose I have the following (silly) identity function:<br>
<br>
   id : Bool -> Bool<br>
   id True  = True<br>
   id False = False<br>
<br>
It's easy enough to show that this really is the identity function by <br>
proving:<br>
<br>
  id-id : (b : Bool) -> id b ≡ b<br>
  id-id True  = refl<br>
  id-id False = refl<br>
<br>
This is all easy enough -- but I've been writing a program where there <br>
are quite a few pattern matches of this form, often with the same (up to <br>
implicit arguments) right hand sides. Is there some idiom or eliminator <br>
that can reduce the amount of pattern matching required? I could write <br>
'id-id' using the usual eliminator for booleans, but I still need to <br>
pass in two copies of refl. What are my options for keeping the number <br>
of cases in check? Thanks in advance,<br>
<br>
   Wouter<br>
_______________________________________________<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/mailman/listinfo/agda</a><br>
</blockquote></div>