8000 chore: remove instBEqNat, which is redundant with instBEqOfDecidableEq but not defeq by kim-em · Pull Request #5694 · leanprover/lean4 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

chore: remove instBEqNat, which is redundant with instBEqOfDecidableEq but not defeq#5694

Merged
kim-em merged 5 commits intomasterfrom
instBEqNat
Oct 16, 2024
Merged

chore: remove instBEqNat, which is redundant with instBEqOfDecidableEq but not defeq#5694
kim-em merged 5 commits intomasterfrom
instBEqNat

Commits

Commits on Oct 13, 2024

Commits on Oct 14, 2024

Commits on Oct 16, 2024
0