Skip to content

refactor: remove duplicate type classes in Iris/Std/Classes.lean and reuse definitions from core libraries - #518

Merged
markusdemedeiros merged 12 commits into
leanprover-community:masterfrom
ISTA-PLV:StdClasses
Jul 25, 2026
Merged

refactor: remove duplicate type classes in Iris/Std/Classes.lean and reuse definitions from core libraries#518
markusdemedeiros merged 12 commits into
leanprover-community:masterfrom
ISTA-PLV:StdClasses

Eliminate the redundant `trans` theorem

57563f6
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
build
succeeded Jul 24, 2026 in 2m 15s