search

Beluga-lang / McTT

A bottom-up approach to a verified implementation of MLTT
https://beluga-lang.github.io/McTT/
MIT License
15 stars 2 forks source link

Are we forced to check? #202

Open HuStmpHrrr opened 2 months ago

HuStmpHrrr commented 2 months ago

It appears to me that we can always infer a type. I suppose the final type is not necessary if it's not given? the inference algorithm should always infer the most precise type. Do we have a theorem stating this?

HuStmpHrrr commented 2 months ago

I think that theorem is a variant of https://github.com/Beluga-lang/McLTT/blob/922419255d4e95251c32c234f274c06d7160f58c/theories/Algorithmic/Typing/Lemmas.v#L280-L283

Ailrun commented 2 months ago

We don't need to. I provided it there just as a testing convenience, but one can simulate that with (fun (x : A) -> x) e instead of e : A (or even with the "let binding" @Antoine-something is implementing)