tc

tc copied to clipboard

Long runtime on dag-like terms

2

Since a few weeks ago, the proof for the `char.zero_lt_d800` theorem in the core library has almost a trillion subterms if we count them as a tree: ```lean open expr...

gebner

The C++ kernel is still more trustworthy than the reference type checker, so if the reference type checker fails to type check the standard library it is most likely an...

dselsam