Skip to content

Replace irrelevance with Prop#2998

Draft
jespercockx wants to merge 2 commits into
agda:experimentalfrom
jespercockx:irrelevance-through-prop
Draft

Replace irrelevance with Prop#2998
jespercockx wants to merge 2 commits into
agda:experimentalfrom
jespercockx:irrelevance-through-prop

Also add --prop to docs

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

Annotations

1 warning
check-whitespace
succeeded May 28, 2026 in 5s