Skip to content

Arvid@dexter lemmas and refactorings

Arvid Jakobssonrequested to merge
arvid@dexter-lemmas-and-refactorings into dev

This MR adds some innocuous lemmas and moves the fold_eval_precond tactic to a more practical place.

This is used by dexter in !100

Merge request reports