From: Rodolfo Campos <camposer@gm...>  20130113 17:12:09
Attachments:
Message as HTML

Hello again guys, Now I'm having troubles using fractional values, don't know how to resolve things like 3/2 * K, because we're only able to use INT and NAT values, what I resolved so far, is to replace the above formula by K + K/2, but as you may notice this is rounding the numbers and loosing some precision, is it possible to use real values or something similar? Thanks in advance, best regards, Rodolfo. 
From: Hoang, Thai Son <htson@in...>  20130113 22:43:10

Hi Rodolfo, I know that there are some push for having real numbers using the Theory plugin in Rodin, but I do not know how far that work goes. The best right now is to use context to define rational numbers, operations and axioms about these operations. Below can be a starting point CONTEXT Rational SETS RATIONAL CONSTANTS Frac /* Constructing a rational number from 2 integers */ Rmultiply /* Multiplication for rational numbers */ AXIOMS Frac : INT ** (INT \ {0}) > RATIONAL Rmultiply : RATIONAL ** RATIONAL > RATIONAL END It is not pretty, especially you will need to formulate a number of axioms about rational before you can do some interesting proofs. Cheers, Son On 13 Jan 2013, at 18:11, Rodolfo Campos <camposer@...<mailto:camposer@...>> wrote: Hello again guys, Now I'm having troubles using fractional values, don't know how to resolve things like 3/2 * K, because we're only able to use INT and NAT values, what I resolved so far, is to replace the above formula by K + K/2, but as you may notice this is rounding the numbers and loosing some precision, is it possible to use real values or something similar? Thanks in advance, best regards, Rodolfo.  Master Visual Studio, SharePoint, SQL, ASP.NET<http://ASP.NET>;, C# 2012, HTML5, CSS, MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current with LearnDevNow  3,200 stepbystep video tutorials by Microsoft MVPs and experts. ON SALE this month only  learn more at: http://p.sf.net/sfu/learnmore_123012_______________________________________________ Rodinbsharpuser mailing list Rodinbsharpuser@... https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Rodolfo Campos <camposer@gm...>  20130114 10:20:27
Attachments:
Message as HTML

Thank you very much Son, finally we solved the problem just isolating the variable, making something like: a < 3/2 b <=> 2a < 3b As easy as that, again, thank you very much for your help. Regards, Rodolfo. On Sun, Jan 13, 2013 at 11:42 PM, Hoang, Thai Son <htson@...> wrote: > Hi Rodolfo, > I know that there are some push for having real numbers using the Theory > plugin in Rodin, but I do not know how far that work goes. > The best right now is to use context to define rational numbers, > operations and axioms about these operations. Below can be a starting point > CONTEXT Rational > SETS RATIONAL > CONSTANTS > Frac /* Constructing a rational number from 2 integers */ > Rmultiply /* Multiplication for rational numbers */ > AXIOMS > Frac : INT ** (INT \ {0}) > RATIONAL > Rmultiply : RATIONAL ** RATIONAL > RATIONAL > END > > It is not pretty, especially you will need to formulate a number of > axioms about rational before you can do some interesting proofs. > Cheers, > Son > > > On 13 Jan 2013, at 18:11, Rodolfo Campos <camposer@...<mailto: > camposer@...>> > wrote: > > Hello again guys, > > Now I'm having troubles using fractional values, don't know how to resolve > things like 3/2 * K, because we're only able to use INT and NAT values, > what I resolved so far, is to replace the above formula by K + K/2, but as > you may notice this is rounding the numbers and loosing some precision, is > it possible to use real values or something similar? > > Thanks in advance, best regards, > > Rodolfo. > >  > Master Visual Studio, SharePoint, SQL, ASP.NET<http://ASP.NET>;, C# 2012, > HTML5, CSS, > MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current > with LearnDevNow  3,200 stepbystep video tutorials by Microsoft > MVPs and experts. ON SALE this month only  learn more at: > > http://p.sf.net/sfu/learnmore_123012_______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > > > >  > Master Visual Studio, SharePoint, SQL, ASP.NET, C# 2012, HTML5, CSS, > MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current > with LearnDevNow  3,200 stepbystep video tutorials by Microsoft > MVPs and experts. ON SALE this month only  learn more at: > http://p.sf.net/sfu/learnmore_123012 > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > 