Frédéric Dupuis
Frédéric Dupuis
I changed it to register the simp attribute the easy way (i.e. the way Leo showed us in the demo after we wrote the tactic). This means that now the...
The linter is now complaining about the absence of docstring on the `register_simp_attr` line, but this currently cannot be done.
On the simp attribute, I just copied the string that is passed as an argument to the command into the docstring. I assume that the string that is passed is...
I just implemented the suggestions, and changing the main loop to return an `Option (Simp.Step)`, to be able to distinguish the case where we find nothing to push from the...
Note that I uncovered a missing case when doing one last check: given an expression like `¬(x = 0 → y = 0)`, we have to check that the left...
I'm still skeptical about the unbundled approach given that there is no "historical" reason for it, but now that there is at least a basic API for it I could...
So we really have two decisions to make: (1) whether we go bundled or unbundled, and (2) if we go unbundled, what the naming scheme should be (in the bundled...
This instance scares me a bit. One example where this is the wrong order is linear maps from `E →L[ℂ] E` to `E →L[ℂ] E`, where we often want to...
> Question: this adds several imports to state the theorem. Should it be put elsewhere? The safe answer would be yes!