mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-11 06:14:41 +03:00
19 lines
203 B
Idris
19 lines
203 B
Idris
module Issue524
|
|
|
|
%logging totality 20
|
|
|
|
data Bad = MkBad (Not Bad)
|
|
|
|
hmmm : Bad -> Not Bad
|
|
hmmm (MkBad n) = n
|
|
|
|
ok : Not Bad
|
|
ok bad = hmmm bad bad
|
|
|
|
bad : Bad
|
|
bad = MkBad ok
|
|
|
|
total
|
|
ohno : Void
|
|
ohno = ok bad
|