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; }