Function height_function_ty 

pub fn height_function_ty() -> Expr

HeightFunction : EllipticCurveObj → EllipticPointObj → Real The canonical Néron-Tate height ĥ: E(K̄) → ℝ.