michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
lean2/tests/lean/955.lean

287 lines
34 KiB
Text
Raw Permalink Normal View History

chore(library/pp_options): reduce pp default limits
2016-02-04 22:55:21 +00:00
-*- 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
Reference in a new issue Copy permalink