8000 feat: `opaque_repr` attribute to suppress "trivial structure" opt by digama0 · Pull Request #2292 · leanprover/lean4 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

feat: opaque_repr attribute to suppress "trivial structure" opt#2292

Open
digama0 wants to merge 3 commits intoleanprover:masterfrom
digama0:opaque_repr
Open

feat: `opaque_repr` attribute to suppress "trivial structure" opt#2292
digama0 wants to merge 3 commits intoleanprover:masterfrom
digama0:opaque_repr

Commits
0