aparler/RosettaCodeData
1
0
Fork 0
Code Issues 12 Pull requests 3 Projects Releases Packages Wiki Activity Actions

YAPC::EU 2018 Glasgow Update!

Browse source
This commit is contained in:
Ingy döt Net 2018-08-17 15:15:24 +01:00
parent 22f33d4004
commit 4e2d22a71d
1170 changed files with 15042 additions and 3047 deletions
Download patch file Download diff file Expand all files Collapse all files

16
Task/Extend-your-language/Agda/extend-your-language.agda Normal file
View file

@ -0,0 +1,16 @@
data Bool : Set where
true : Bool
false : Bool
if_then_else : ∀ {l} {A : Set l} -> Bool -> A -> A -> A
if true then t else e = t
if false then t else e = e
if2_,_then_else1_else2_else_ : ∀ {l} {A : Set l} -> (b1 b2 : Bool) -> (t e1 e2 e : A) -> A
if2 true , true then t else1 e1 else2 e2 else e = t
if2 true , false then t else1 e1 else2 e2 else e = e1
if2 false , true then t else1 e1 else2 e2 else e = e2
if2 false , false then t else1 e1 else2 e2 else e = e
example : Bool
example = if2 true , false then true else1 false else2 true else false