Relationship between `let` and `match`

Stream: general

[nrs]

Do we have, in all cases, that fun (A : Type) => let a := A; _ and fun (A : Type) => match A with | a => _ result in a := A? Is this true even if A : something where something is not Type?

[Mario Carneiro]

no, match A with | a => _ is like have a := A; _ not let

[Mario Carneiro]

the difference is that inside the body of the _ you will not be able to know that a := A

[nrs]

Mario Carneiro said:

no, match A with | a => _ is like have a := A; _ not let

I see, thanks a lot for the help!!