Simon Hudon
So far so good. I followed the instruction for `cmake` and I added a call to `vcpkg` in my appveyor script. `cmake` doesn't seem to be finding `dlfcn-win32`. How do...
What would you do when you add a second package that specifies a different version of Lean?
Sorry! I must have missed that!
Specifically, @digama0 pointed out that redefining `of_repeat` fixes the problem: ```lean def of_repeat {n i} : repeat n Prop i → Prop := begin induction i with n i IH,...
I think `target'` should not replace target. We don't need to instantiate mvars and normalize the goal every time we query it. It is a much slower version of `target`.
One thing it might (or might not) be a problem for is that we could want to generate `.olean` files from other source languages than Lean (for instance, C++ or...
I meant the change in the default behavior. The point about the build system is reasonable. We could also make the flag available as `set_option` or even just allow one...
Written together with @danielfabian
I don't think this should be considered a bug. The term is traversed completely at every pass of `simp` and every pass meets only one opportunity for rewrite. I pointed...