fact: Fixpoint cont_to_pfunct (r : cont_function) : PartIR := match r with | hyp_c Hab F H => F | hyp_d Hab F F' H => F | hyp_d' Hab F F' H => F' | hyp_diff Hab F H => F | cconst c => [-C-]c | cid => FId | cplus f g => cont_to_pfunct f{+}cont_to_pfunct g | cinv f => {--}(cont_to_pfunct f) | cminus f g => cont_to_pfunct f{-}cont_to_pfunct g | cmult f g => cont_to_pfunct f{*}cont_to_pfunct g | cscalmult c f => c{**}cont_to_pfunct f | cnth f n => cont_to_pfunct f{^}n | cabs f => FAbs (cont_to_pfunct f) end.
imports: CoRN.ftc.Differentiability