Simon Hudon
This issue made me realize that the syntax for `struct` is not the same as in `Fixpoint` definitions. This page of documentation http://mattam82.github.io/Coq-Equations/examples/Examples.nested_mut_rec.html refers to `struct` without giving the actual...
Here is how I use it to improve my workflow with the Iris Proof Mode (IPM). Iris encodes different kinds of assumptions in the conclusion of a goal so the...
So the short answer to your question is: by writing a regexp that will match a piece of the goal
One more note: I made sure that the default has the same behavior as the current version.
I'd like to echo this request. `ccache` seems like a great tool and I'd love to be able to use it with a Lean project http://leanprover.github.io/ instead of C++, etc....
`sorry` creates a warning and in trust level 0, it creates an error. Additionally, when you use `sorry`, you can use the definition / lemma after but with abort, the...
One way I have been producing a similar effect is with: ```lean example : true := begin suffices : /- some formula -/, trivial, /- a proof that you can...
Also, I'd like to add that development on Lean 3 have moved to https://github.com/leanprover-community/lean. This is where we put bug fixes and new features.
Development of Lean 3 has stopped as the developers focus on Lean 4. You can post your issue on the community fork of Lean instead: https://github.com/leanprover-community/lean/issues. But the short answer...
Can you repost to https://github.com/leanprover-community/lean? This is where we handle bug fixes now.