mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-17 08:11:45 +03:00
12 lines
202 B
Idris
12 lines
202 B
Idris
|
module Issue660
|
||
|
|
|
||
|
|
%default total
|
||
|
|
|
||
|
|
%logging declare.data.parameters 20
|
||
|
|
|
||
|
|
data C : Type -> Type where
|
||
|
|
MkC : List a -> C a
|
||
|
|
|
||
|
|
data D : Type -> Type where
|
||
|
|
MkD : {0 a : Type} -> let 0 b = List a in b -> D a
|