minitt::type_check
pub fn check( index: u32, (gamma, context): TCS, expression: Expression, value: Value) -> TCM<TCS>
check in Mini-TT. However, telescope and gamma are preserved for REPL use.
check