<div dir='auto'>Thanks, Nils.<div dir="auto">Is there an equivalent to the Idris case-of statement in Agda?</div></div><div class="gmail_extra"><br><div class="gmail_quote">Le 15 avr. 2020 22:10, Nils Anders Danielsson <nad@cse.gu.se> a écrit :<br type="attribution" /><blockquote class="quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><p dir="ltr">On 2020-04-15 22:07, Philippe de Rochambeau wrote: <br>
> StringOrInt : ∀ {ℓ} {A : Set ℓ} → Bool → A <br>
> StringOrInt True  = Nat <br>
> StringOrInt False = String <br>
<br>
StringOrInt : Bool → Set <br>
StringOrInt true  = Nat <br>
StringOrInt false = String <br>
<br>
--  <br>
/NAD <br>
</p>
</blockquote></div><br></div>