Skip to content

feat: remaining introduction patterns and case destruction patterns#496

Open
alvinylt wants to merge 53 commits into
leanprover-community:masterfrom
ISTA-PLV:IntroPats
Open

feat: remaining introduction patterns and case destruction patterns#496
alvinylt wants to merge 53 commits into
leanprover-community:masterfrom
ISTA-PLV:IntroPats

Generalise `Hyps.add` and `Hyps.addWithInfo` to resolve two TODO items

c59afb6
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
build-math
succeeded Jul 3, 2026 in 4m 30s