<div dir='auto'>Hi James,<div dir="auto">wonderful.</div><div dir="auto">I'm really enjoying learning Agda.</div><div dir="auto">Goodnight to all.</div><div dir="auto">Philippe </div></div><div class="gmail_extra"><br><div class="gmail_quote">Le 15 avr. 2020 22:27, James Wood <james.wood.100@strath.ac.uk> 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">Hi and welcome, Philippe,</p>
<p dir="ltr">Agda's standard library implements `case` statements via mixfix syntax<br>
and pattern-matching λ-abstractions. See<br>
https://agda.github.io/agda-stdlib/README.Case.html for examples.</p>
<p dir="ltr">Best,</p>
<p dir="ltr">James</p>
<p dir="ltr">On 15/04/2020 21:22, phiroc@free.fr wrote:<br>
> Thanks, Nils.<br>
> Is there an equivalent to the Idris case-of statement in Agda?<br>
> <br>
> Le 15 avr. 2020 22:10, Nils Anders Danielsson <nad@cse.gu.se> a écrit :<br>
> <br>
>     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>
> <br>
> <br>
> <br>
> _______________________________________________<br>
> Agda mailing list<br>
> Agda@lists.chalmers.se<br>
> https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&amp;data=02%7C01%7Cjames.wood.100%40strath.ac.uk%7Ca81a61430d464ed3e31808d7e17ab5dd%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637225789472118838&amp;sdata=EqKo%2FI7beR4l3OJt7pIfx0yq7TT7l55wjnhjtLCEBes%3D&amp;reserved=0<br>
> <br>
_______________________________________________<br>
Agda mailing list<br>
Agda@lists.chalmers.se<br>
https://lists.chalmers.se/mailman/listinfo/agda<br>
</p>
</blockquote></div><br></div>