Skip to content

Commit

Permalink
feat(equiv/basic): use @[simps] (#4652)
Browse files Browse the repository at this point in the history 
Use the `@[simps]` attribute to automatically generate equation lemmas for equivalences.
The names `foo_apply` and `foo_symm_apply` are used for the projection lemmas of `foo`.
  • Loading branch information
@fpvandoorn
fpvandoorn committed Oct 28, 2020
1 parent e8f8de6 commit 40da087
Show file tree
Hide file tree
Showing 4 changed files with 68 additions and 165 deletions.

0 comments on commit 40da087

Please sign in to comment.