notation "a '"
non associative with precedence 80
for @{ 'deriv $a }.
-interpretation "function derivative" 'deriv x =
- (cic:/matita/didactic/deriv/De.con x).
-interpretation "function mult" 'mult x y =
- (cic:/matita/didactic/deriv/fmult.con x y).
-interpretation "function compositon" 'compose x y =
- (cic:/matita/didactic/deriv/fcomp.con x y).
+interpretation "function derivative" 'deriv x = (De x).
+interpretation "function mult" 'mult x y = (fmult x y).
+interpretation "function compositon" 'compose x y = (fcomp x y).
notation "hvbox(a break + b)"
right associative with precedence 45
for @{ 'oplus $a $b }.
-interpretation "function plus" 'plus x y =
- (cic:/matita/didactic/deriv/fplus.con x y).
+interpretation "function plus" 'plus x y = (fplus x y).
axiom i:R→F. (*mappatura R in F*)
coercion cic:/matita/didactic/deriv/i.con.
notation "ρ"
non associative with precedence 100
for @{ 'rho }.
-interpretation "function flip" 'rho =
- cic:/matita/didactic/deriv/freflex.con.
+interpretation "function flip" 'rho = freflex.
axiom reflex_ok: ∀f:F. ρ ∘ f = (i (-R1)) · f.
axiom dereflex: ρ ' = i (-R1). (*Togliere*)
right associative with precedence 75
for @{ 'elev $a $b }.
-interpretation "function power" 'elev x y =
- (cic:/matita/didactic/deriv/felev.con x y).
+interpretation "function power" 'elev x y = (felev x y).
axiom tech1: ∀n,m. F_OF_nat n + F_OF_nat m = F_OF_nat (n + m).