Prove-It
Prove-It copied to clipboard
sandialabs
A tool for proving and organizing general theorems using Python.
In some of the proof notebook titles, underscores appearing in theorem names are being misinterpreted (looks like they're being interpreted, sometimes, as flags for italics). As an example, consider the...
One cannot distinguish between a Literal and its corresponding Variable form by looking at them and this can be confusing. We can take steps to avoid confusion, however. 1) Raise...
It would be very useful to see the LaTeX form of expressions when they are referenced in exception messages, where possible. Sometimes the LaTeX cannot be generated or compiled, in...
This is a principle I've been thinking about recently that we should discuss. The problem is that improvements in automation can break existing proofs. As the system grows, this is...
I was recently reviewing (admittedly at a fairly superficial level) polymorphism in Coq's Gallina language and just today was also reviewing the `Max` and `Min` classes in Prove-It where I...
Auto-simplification is turned off while deriving side-effects to avoid infinite recursion issues. I ran into an instance where it was prudent to turn it on for a particular side-effect. Maybe...
For example, it is easy to use Add, Mult, Sum, etc instead of VecAdd, ScalarMult, VecSum, etc. These are intentionally different types of Expressions because functionality needs to be different,...
Rather than requiring a rebuild when the __pv_it directories are out-of-date, it would be nice to automatically execute the dependent notebooks to bring things up-to-date as needed. Relates to #86.
@jmadridlarra ran into this issue while trying to change the style of an inner expression.
Otherwise, this leads to non-intuitive effects of changing the style on past expressions.
Metadata
Owner
Metadata
A tool for proving and organizing general theorems using Python.