From 45727df35e5ac99ba037318d216210c24ff706ad Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 30 Nov 2006 21:55:07 +0000 Subject: [PATCH] I have changed the nice notation for derivatives a little bit to always pick 'x' as the default variable. This is the only reasonable choice since we already always pick 'x' for polynoms. --- matita/library/demo/power_derivative.ma | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/matita/library/demo/power_derivative.ma b/matita/library/demo/power_derivative.ma index ce288b731..879f55d7e 100644 --- a/matita/library/demo/power_derivative.ma +++ b/matita/library/demo/power_derivative.ma @@ -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. -- 2.39.2