New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

unreachable code was reached on some machines #6

Open

fpvandoorn opened this issue Jun 16, 2017 · 0 comments

fpvandoorn commented Jun 16, 2017 •

edited

Loading

In the commit d38979f 'unreachable' code was reached when elaborating this theorem on some machines:

lean2/hott/types/trunc.hlean

Line 299 in d38979f

    
           theorem is_trunc_trunctype [instance] (n : ℕ₋₂) : is_trunc n.+1 (n-Type) :=

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

The text was updated successfully, but these errors were encountered:

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment