mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-21 02:31:50 +03:00
11 lines
249 B
Idris
11 lines
249 B
Idris
|
test : List Nat -> List Nat
|
||
|
|
test [] = []
|
||
|
|
test (n :: ns) = ?n :: ns
|
||
|
|
|
||
|
|
replicate : (n : Nat) -> a -> List a
|
||
|
|
replicate Z a = []
|
||
|
|
replicate (S n) a = a :: replicate n a
|
||
|
|
|
||
|
|
testReplicate : test (replicate (1+n) k) === replicate (2+n) k
|
||
|
|
testReplicate = ?goal
|