Skip to content

GitLab

I
Iris
Merged
Opened by Robbert@robbertkrebbersMaintainer
Report abuse

Alternative take on making proof mode terms more compact.

This is an alternative to !224 (closed) by splitting up envs_lookup_delete premises into envs_lookup and envs_delete.

@jtassaro Could you rebase !224 (closed) so we can compare?

The following tactics involve some other tricks:

  • tac_assumption: uses a let binding for envs_delete since its result is used twice
  • tac_specialize: uses a let binding for envs_delete since its result is used twice
  • tac_specialize_assert: uses a conjunction, not sure if it's worth the extra bloat in the Ltac code to do something smarter here.
Edited by Robbert