lean2 icon indicating copy to clipboard operation
lean2 copied to clipboard

unreachable code was reached on some machines

Open fpvandoorn opened this issue 7 years ago • 0 comments

In the commit https://github.com/leanprover/lean2/commit/d38979f783416c3b2a3a608640b8cf1e243770d6 'unreachable' code was reached when elaborating this theorem on some machines: https://github.com/leanprover/lean2/blob/d38979f783416c3b2a3a608640b8cf1e243770d6/hott/types/trunc.hlean#L299 I worked around it by rewriting the proof in the two commits after that.

This error occurred on a machine with Ubuntu 17.04 with g++ 6.3.0 or with g++ 5.4.1 (I believe) and on a mac (with unknown version gcc/g++).

There were no errors on a machine with Ubuntu 16.04 with gcc 5.4.0/g++ 5.4.0

fpvandoorn avatar Jun 16 '17 19:06 fpvandoorn