[Agda] StringOrInt function

Nils Anders Danielsson nad at cse.gu.se
Wed Apr 15 22:10:07 CEST 2020


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


More information about the Agda mailing list