mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-10-27 06:29:52 +03:00
25 lines
366 B
Idris
25 lines
366 B
Idris
module Issue1236
|
|
|
|
private
|
|
data Mismatched1 : Type
|
|
export
|
|
data Mismatched1 : Type where
|
|
|
|
public export
|
|
data Mismatched2 : Type
|
|
export
|
|
data Mismatched2 : Type where
|
|
|
|
export
|
|
data Aligned : Type
|
|
export
|
|
data Aligned : Type where
|
|
|
|
public export
|
|
data SpecifyOnce1 : Type
|
|
data SpecifyOnce1 : Type where
|
|
|
|
data SpecifyOnce2 : Type
|
|
public export
|
|
data SpecifyOnce2 : Type where
|