15 lines
312 B
Agda
15 lines
312 B
Agda
module AutoInData
|
|
|
|
import Prelude
|
|
|
|
rep : ∀ a. Nat → a → List a
|
|
rep Z x = Nil
|
|
rep (S k) x = x :: rep k x
|
|
|
|
data RunLength : ∀ ty. List ty → U where
|
|
Empty : ∀ ty. RunLength {ty} Nil
|
|
Run : ∀ ty more. (n : Nat) →
|
|
(x : ty) →
|
|
RunLength more →
|
|
RunLength (rep n x ++ more)
|