Add typechecker DRT target that ensures the same typed expression is computed

[lianah]

Category

DRT target(s)

Describe the feature you'd like to request

We should add a new DRT target that ensures that the Rust typecheck_by_single_request_env and the Lean Validator.typecheckPolicy compute the same well typed expression when successful.

Describe alternatives you've considered

Do not add this target.

Additional context

See 839 for a related target that checks that the types computed for an expression match.

Is this something that you'd be interested in working on?

• 👋 I may be able to implement this feature request
• ⚠️ This feature might incur a breaking change