[Agda] StringOrInt function

[James Wood]

Hi and welcome, Philippe,

Agda's standard library implements `case` statements via mixfix syntax
and pattern-matching λ-abstractions. See
https://agda.github.io/agda-stdlib/README.Case.html for examples.

Best,

James

On 15/04/2020 21:22, phiroc at free.fr wrote:
> Thanks, Nils.
> Is there an equivalent to the Idris case-of statement in Agda?
> 
> Le 15 avr. 2020 22:10, Nils Anders Danielsson <nad at cse.gu.se> a écrit :
> 
>     On 2020-04-15 22:07, Philippe de Rochambeau wrote:
>     > StringOrInt : ∀ {ℓ} {A : Set ℓ} → Bool → A
>     > StringOrInt True  = Nat
>     > StringOrInt False = String
> 
>     StringOrInt : Bool → Set
>     StringOrInt true  = Nat
>     StringOrInt false = String
> 
>     -- 
>     /NAD
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=02%7C01%7Cjames.wood.100%40strath.ac.uk%7Ca81a61430d464ed3e31808d7e17ab5dd%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637225789472118838&sdata=EqKo%2FI7beR4l3OJt7pIfx0yq7TT7l55wjnhjtLCEBes%3D&reserved=0
>