]> matita.cs.unibo.it Git - helm.git/commitdiff
I have changed the nice notation for derivatives a little bit to always pick
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 30 Nov 2006 21:55:07 +0000 (21:55 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 30 Nov 2006 21:55:07 +0000 (21:55 +0000)
'x' as the default variable. This is the only reasonable choice since we already
always pick 'x' for polynoms.

helm/software/matita/library/demo/power_derivative.ma

index ce288b731ad998b959d2c71b8cc74455b79daff9..879f55d7e4976227c48756d39a626a1120d12147 100644 (file)
@@ -281,6 +281,7 @@ clear H.
   done.
 qed.
 
+(*
 notation "hvbox(\frac 'd' ('d' ident i) break p)"
   right associative with precedence 90
 for @{ 'derivative ${default
@@ -289,6 +290,14 @@ for @{ 'derivative ${default
 
 interpretation "Rderivative" 'derivative \eta.f =
  (cic:/matita/demo/power_derivative/derivative.con f).
+*)
+
+notation "hvbox(\frac 'd' ('d' 'x') break p)"
+  right associative with precedence 90
+for @{ 'derivative $p}.
+
+interpretation "Rderivative" 'derivative f =
+ (cic:/matita/demo/power_derivative/derivative.con f).
 
 theorem derivative_power': ∀n:nat. D[x \sup (1+n)] = (1+n)*x \sup n.
  assume n:nat.