Mario Carneiro
Mario Carneiro
I have a version of leangz I would like to test, but this PR has no working pr-release AFAICT
Okay, https://github.com/digama0/leangz/compare/olean2 seems to work based on a manually built lean executable using this PR. But I did notice one issue: Currently, manually built lean executables have the `lean_version` field...
Note, to fix this issue I think it suffices to ensure that any non-official release has a `lean_version` string not matching the regex `[0-9]+\.[0-9]+\.[0-9]+(-rc[0-9]+)?`. For example, using the lean-toolchain name...
I don't think it's that simple. Most functions don't have the ability to do precomputation, writing `let x := precomputed; fun y => f x y` doesn't do what you...
> > Most functions don't have the ability to do precomputation, writing let x := precomputed; fun y => f x y doesn't do what you think it does >...
I believe that this kind of thing *is* regarded as a compiler bug, or at least a thing worth improving, but the compiler is on hold and has been for...
> so it's only a matter of disabling or changing the offending transformations. You are very much underestimating the amount of work this is. The compiler does this eta expansion...
This design makes it impossible to indent the first line.
> > This design makes it impossible to indent the first line. > > Yes, it's designed to handle code, and in languages where whitespace is signficant (eg. python) indentation...
By my reading of the proposal the string literal would be an error because the second line is less indented than the first.