2013-09-07 01:31:47 +00:00
|
|
|
|
Set: pp::colors
|
|
|
|
|
|
Set: pp::unicode
|
|
|
|
|
|
Assumed: vector
|
|
|
|
|
|
Assumed: N0
|
|
|
|
|
|
Proved: V0
|
|
|
|
|
|
Assumed: f
|
|
|
|
|
|
Assumed: m
|
|
|
|
|
|
Assumed: v1
|
|
|
|
|
|
Error (line: 12, pos: 6) type mismatch at application
|
|
|
|
|
|
f m v1
|
|
|
|
|
|
Function type:
|
2013-09-08 18:04:07 +00:00
|
|
|
|
Π (n : ℕ), (vector ℤ n) → ℤ
|
2013-09-07 01:31:47 +00:00
|
|
|
|
Arguments types:
|
|
|
|
|
|
m : ℕ
|
|
|
|
|
|
v1 : vector ℤ (m + 0)
|
2013-09-09 05:54:22 +00:00
|
|
|
|
f m (cast (V0 ℤ m) v1) : ℤ
|
