mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-25 22:06:33 +03:00
24 lines
693 B
Plaintext
24 lines
693 B
Plaintext
id : {0 a : Type} -> a -> a
|
|
id = \ x : _ => x
|
|
|
|
idid : {0 a : Type} -> a -> a
|
|
idid = id id id id id id id id
|
|
id id id id id id id id id id
|
|
id id id id id id id id id id
|
|
id id id id id id id id id id
|
|
id id id id id id id id id id
|
|
id id id id id id id id id id
|
|
id id id id id id id id id id
|
|
id id id id id id id id id id
|
|
id id id id id id id id id id
|
|
id id id id id id id id id id
|
|
id id id id id id id id id id
|
|
id id id id id id id id id id
|
|
id id id id id id id id id id
|
|
id id id id id id id id id id
|
|
id id id id id id id id id id
|
|
id id id id id id id id id id
|
|
|
|
idTy : Type
|
|
idTy = idid Type
|