# Conv


Checks whether two values are definitionally equal at a given
binding depth. Purely structural — no type information used, no
eta expansion. Pure function — part of the TCB.

## Core Functions

- `conv : Depth → Val → Val → Bool` — check definitional equality.
- `convSp : Depth → Spine → Spine → Bool` — check spine equality
  (same length, pairwise `convElim`).
- `convElim : Depth → Elim → Elim → Bool` — check elimination frame
  equality (same tag, recursively conv on carried values).

## Conversion Rules

- **Structural**: same-constructor values with matching fields.
  Universe levels compared by `==`. Primitive literals by value.
- **Binding forms**: Pi, Lam, Sigma compared under a fresh
  variable at depth d (instantiate both closures, compare at d+1).
- **Compound values**: recursive on all components.
- **Neutrals**: same head level and convertible spines.
- **Catch-all**: different constructors → false.

## Trampolining

Deep ordinary data is represented by generated `VDescCon` values.
Conversion stays structural except for explicitly documented
eta/unfolding rules.

## No Eta

`conv` does not perform eta expansion: a neutral `f` and
`λx. f(x)` are **not** definitionally equal. Cumulativity
(`U(i) ≤ U(j)`) is handled in check.nix, not here.

## `admitLevel`

_admitLevel: is a Level term-independent? — every `normLevel` summand rests on a `zero` or empty-spine `var` base; the shared predicate behind every universe-level soundness gate. Rejects applied-neutral bases, admits level variables._

```
admitLevel : Val -> Bool
```

## `cPeelArm`

_cPeelArm: deep-arm classifier for `cPeel` — peels VNe spines and VMu/VDesc/VBootEq towers onto the machine frontier via the shared `elimGoals` decomposition. Returns a layer record or null._

```
cPeelArm : Depth -> Val -> Val -> ({ kind; goals; na; nb; nd; } | null)
```

## `cPeelBinder`

_cPeelBinder: binder-arm classifier for `cPeel` — mirrors convStep's VPi/VLam/eta/VSigma arms (and the preceding Lift-collapse guard) so binder layers peel flat. Returns a layer record or null._

```
cPeelBinder : Depth -> Val -> Val -> ({ kind; goals; na; nb; nd; } | null)
```

## `conv`

_conv: definitional equality on values at binding `depth` — purely structural with Σ/Unit/Π-eta; foundation of `Sub` in `check` and the kernel TCB._

```
conv : Depth -> Val -> Val -> Bool
```

## `convElim`

_convElim: elimination-frame equality at binding `depth` — same tag and recursively `conv` on every carried value; building block of `convSp`._

```
convElim : Depth -> Elim -> Elim -> Bool
```

## `convLevel`

_convLevel: definitional equality on Level expressions — `normLevel` both sides, then structural compare; required because `convLevel` is non-trivial under `levelMax` associativity._

```
convLevel : Val -> Val -> Bool
```

## `convSp`

_convSp: spine equality at binding `depth` — same length plus pairwise `convElim` on each frame; used to compare two neutral-value spines._

```
convSp : Depth -> Spine -> Spine -> Bool
```

## `convStep`

_convStep: single conversion step over forced values — the conv dispatch body, called by the `runConvF` machine for non-structural goals._

```
convStep : Depth -> Val -> Val -> Bool
```

## `normLevel`

_normLevel: normalise a Level expression to canonical form — `levelMax`/`levelSuc` collapsed via the algebraic laws so two equivalent forms compare equal under `convLevel`._

```
normLevel : Val -> Val
```