Skip to content

Simple changes to make proof mode terms more compact

Joseph Tassarotti requested to merge ci/joe/compact_ipm_simple into master

This MR takes some of the simpler, less controversial changes from !224 (closed) to make proof terms compact. In particular, it only converts tactics where we can straightforwardly avoid the issue with conjunctions pointed out by @robbertkrebbers in !224 (comment 35229). Although subsequent discussion in that MR considers ways to work around those issues, it is not clear what the best solution is. Therefore, it seemed better to make a separate MR to merge the easy changes and then later figure out what to do with the other tactics.

This MR still gives a 9.63% improvement on lambda-rust, while !224 (closed) gives 16.70%.

The plan is to rebase it after !247 (merged) is merged.

Edited by Joseph Tassarotti

Merge request reports