lean2

lean2 copied to clipboard

chore(lp): fix compilation error

2

``` /build/source/src/util/lp/permutation_matrix.h:126:44: error: cannot convert 'const std::vector' to 'unsigned int*' in return 126 | unsigned * values() const { return m_permutation; } | ^~~~~~~~~~~~~ | | | const std::vector ```...

collares

Align the result of `operator new` to `alignof(max_align_t)`

1

The C++ spec requires the result of `operator new` to be aligned to `alignof(max_align_t)`, which is 16 on x86_64 Linux. However, lean's `operator new` returns 8 byte aligned memory under...

tzik

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....

fpvandoorn