pub fn recheck(ctx: &Context, term: &Term) -> Result<Term, ReCheckError>Expand description
Independently re-check term in ctx, returning its inferred type on success.
A SEPARATE implementation from infer_type: a de Bruijn core
(now including the Match eliminator) with its own reduction and cumulative
conversion, so a bug in one checker is unlikely to be shared by the other. Returns
ReCheckError::Unsupported for the fragment it does not yet cover (Fix/Hole,
or an unrecognized inductive) — never a false pass.