smooth vector field on manifold

Stream: Is there code for X?

[Winston Yin]

How would one express a smooth section of the tangent bundle of a smooth manifold? Suppose the manifold M is modelled on a real vector space E, would (v : M → E) (hv : cont_mdiff I 𝓘(ℝ, E) ⊤ v) have the right meaning?