# CheckD


checkD: generic bidirectional checker for Desc payloads — validates terms against `interpD level I D X i` by walking the description.

## `checkD`

_checkD: check a payload term against the interpretation of a description at a concrete index and recursive family._

```
checkD : Ctx -> Level -> I -> D -> X -> i -> Tm -> Computation Tm
```

## `checkDAt`

_checkDAt: spec-record variant of checkD; spec contains `{ level; I; D; X; i; }`._

```
checkDAt : Ctx -> { level; I; D; X; i; } -> Tm -> Computation Tm
```

## `inferD`

_inferD: synthesize the checked payload and its `interpD level I D X i` type._

```
inferD : Ctx -> Level -> I -> D -> X -> i -> Tm -> Computation { term; type; }
```

## `inferDAt`

_inferDAt: spec-record variant of inferD; spec contains `{ level; I; D; X; i; }`._

```
inferDAt : Ctx -> { level; I; D; X; i; } -> Tm -> Computation { term; type; }
```