Behaviour of type checking / infering functions

Stream: lean4

[Mathis Bouverot-Dupuis]

Hello ! I'm wondering which functions I should use to typecheck/type infer some Exprs :

• Meta.check seems to do full type checking, assigning metavars if needed
• Meta.inferTypeseems to expect its argument to be well-typed already, and does not attempt to assign any metavars

[Mathis Bouverot-Dupuis]

Is this correct ?

[Kyle Miller]

I'm not sure that inferType doesn't incidentally assign metavariables, but you are correct that it assumes its argument is type-correct, and it's not meant for assigning metavariables. These are the correct functions for checking and inference.

I think the same is true about Meta.check, where it incidentally assigns metavariables, but it's not meant to be used for that.