inductive types (W)
maybe this can be a quantity that is treated specially on the head of a case expression
inductive types (W)
it's like. the normal case rules are
\frac{
\begin{gathered}
Ψ \mid Γ ⊢ σ · e ⇒ A \rhd Θ' \qquad
Ψ \mid Γ, x:A ⊢₀ C ⇐ ★ \\
\overline{Ψ \mid Γ ⊢ σ…
quotient types
some notes i found in my home folder
syntax (placeholder)
\begin{aligned}
s, t, p, A, B, R &::= \cdots \mid A⇂R \mid
the function part of a w value probably needs to be ω
inductive types (W)
inlining #24 here to reduce clutter
a binary tree is something like (in hypothetical future quox with implicits and λcase)
def0 Tag = {leaf, node}
def0 Field : Tag → ★…