286 lines
34 KiB
Text
286 lines
34 KiB
Text
-*- mode: compilation; default-directory: "~/projects/lean/tests/lean/run/" -*-
|
|
Compilation started at Thu Feb 4 14:53:07
|
|
|
|
/home/leo/projects/lean/bin/lean -Dpp.width=120 /home/leo/projects/lean/tests/lean/run/955.lean
|
|
/home/leo/projects/lean/tests/lean/run/955.lean:31:32: error: type mismatch at definition 'append_auxH', has type
|
|
@vectorH.{?M_1}
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(…
|
|
…))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
|
|
?M_4
|
|
but is expected to have type
|
|
@vectorH.{?M_1}
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(…
|
|
…))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
|
|
(@vector.append_aux.{?M_1+1} Type.{?M_1} nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(nat.addl
|
|
nat.zero
|
|
(…
|
|
…))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
|
|
(@vector.nil.{?M_1+1} Type.{?M_1})
|
|
?M_3)
|
|
The following identifier(s) are introduced as free variables by the left-hand-side of the equation:
|
|
v'
|
|
|
|
Compilation exited abnormally with code 1 at Thu Feb 4 14:53:09
|