feat: theorems are opaque#12973

Merged

nomeata merged 5 commits intomasterfrom

joachim/opaque-thm

Mar 23, 2026

Commits on Mar 18, 2026

feat: make theorems opaque in kernel and elaborator

nomeata
and
claude
committed
refactor: simplify FunInd theorem unfolding to plain delta+beta

nomeata
and
claude
committed
refactor: split test, revert unnecessary allowOpaque in simp

nomeata
and
claude
committed

Commits on Mar 19, 2026

feat: add `allowOpaque` parameter to `delta?` and `deltaExpand`

nomeata
and
claude
committed

Commits on Mar 23, 2026

Apply suggestions from code review
nomeata
authored