Skip to content

[Merged by Bors] - chore: fix some ENat-related instances of backward.isDefEq.respectTransparency#41515

Closed
vlad902 wants to merge 2 commits into
leanprover-community:masterfrom
vlad902:respect-transparency5
Closed

[Merged by Bors] - chore: fix some ENat-related instances of backward.isDefEq.respectTransparency#41515
vlad902 wants to merge 2 commits into
leanprover-community:masterfrom
vlad902:respect-transparency5

fix unused simp lemma

a9cf1d2
Select commit
Loading
Failed to load commit list.
Sign in for the full log view

Annotations

1 warning
main
succeeded Jul 9, 2026 in 26s