-- -- Inverse -- inverse t f x := match f as mathExpr with | ?isSimpleTerm -> match f as symbolExpr with | #x -> t | #exp #x -> log t | #log #x -> exp t | #sqrt #x -> t ^ 2 | #cos #x -> acos t | #sin #x -> asin t | #acos #x -> cos t | #asin #x -> sin t | _ -> inverse' t f x -- TODO: define inverse' | ?isTerm -> match f as termExpr with | term #1 (ncons $n #x []) -> rt n t | term _ (ncons $n #x _) -> let a := f / x ^ n in inverse (t / a) (f / a) x | _ -> `inverse t f x | ?isPolynomial -> match coefficients x f as list mathExpr with | $c :: (loop $i (1, $n) (#0 :: ...) ($a :: [])) -> inverse ((t - c) / a) (x ^ (n + 1)) x | _ -> `inverse t f x | _ -> match f as mathExpr with | $p1 / $p2 -> inverse (p2 * t) p1 x | _ -> `inverse t f x