Skip to content

Commit

Permalink
chore: remove dead code in Fin2.lean
Browse files Browse the repository at this point in the history 
We've duplicated a lot of API of `Fin2` for `PFin2`, but this is not really necessary.
  • Loading branch information
@alexkeizer
alexkeizer committed Feb 18, 2024
1 parent f2cd0be commit 7e50897
Show file tree
Hide file tree
Showing 2 changed files with 45 additions and 349 deletions.
Loading

0 comments on commit 7e50897

Please sign in to comment.