Proposition for a almost-bitsize-independent Int31.v (joint work with J. Vouillon)

As said at the beginning of the file: 

  This file contains basic definitions of a 31-bit integer
  arithmetic. In fact it is more general than that. The only reason
  for this use of 31 is the underlying mecanism for hardware-efficient
  computations by A. Spiwack. Apart from this, a switch to, say,
  63-bit integers is now just a matter of replacing every occurences
  of 31 by 63. This is actually made possible by the use of
  dependently-typed n-ary constructions for the inductive type
  [int31], its constructor [I31] and any pattern matching on it.
  If you modify this file, please preserve this genericity. 

From the user point-of-view, almost nothing has changed: functions
like On, In, shiftr, shiftl and a few others now have a
syntactically-different definition, but thanks to Eval compute in their
definition, this leads to the exact same coq objects as before. The only
difference is "Check I31" that shows the compact n-ary version 
(nfun digits 31 int31) instead of (digits -> ... -> digits -> int31).
But even "Print int31" shows the same answer as before (the above type
of I31 is shown after expansion). 

Arnaud, could you check whether all this works fine with your
retroknowledge ?

Notice the new file NaryFunction that contain generic stuff about
n-ary dependent functions. It should end some day in another place
than theories/Numbers, but I cant figure where for now. This file is
also quite skinny yet, but it's a start.




git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10967 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions