Skip to content

Commit

Permalink
noprime
Browse files Browse the repository at this point in the history
  • Loading branch information
@YaelDillies
YaelDillies committed Oct 9, 2024
1 parent 56ae59c commit e5f13fc
Showing 1 changed file with 3 additions and 0 deletions.
3 changes: 3 additions & 0 deletions scripts/no_lints_prime_decls.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1128,6 +1128,9 @@ EMetric.diam_union'
EMetric.mem_ball'
EMetric.mem_closedBall'
EMetric.totallyBounded_iff'
ENat.add_biSup'
ENat.biSup_add'
ENat.biSup_add_biSup_le'
ENat.sSup_eq_zero'
Encodable.mem_decode₂'
ENNReal.add_biSup'
Expand Down

0 comments on commit e5f13fc

Please sign in to comment.