9 lines
108 B
Agda
9 lines
108 B
Agda
module LitConCase
|
|
|
|
data Unit = MkUnit
|
|
|
|
foo : Int → Unit
|
|
foo 0 = MkUnit
|
|
foo MkUnit = MkUnit
|
|
foo _ = MkUnit
|