Make irrelevant-recompute unsafe - #3012

Open

jespercockx wants to merge 2 commits into

experimentalfrom

unsafe-recompute

Commits on Jun 10, 2026

[ re agda/#8557 ] Move irrelevant-recompute and corollaries to Unsafe module with --irrelevant-projections flag
jespercockx
committed
9a543dc

Commits on Jun 11, 2026

[ re agda/#8557 ] Restore ⊥-recompute and ¬-recompute as safe
jespercockx
committed
5f11340