Commits · e77e434d7e62c886b060472fefe1a26b8e2156ea · Flocq / flocq · GitLab

11 May, 2010 1 commit
- Added Rcompare_Eq_inv. · e77e434d
  Guillaume Melquiond authored May 11, 2010
  
  e77e434d
23 Apr, 2010 3 commits
- Started proof of generic_NE_pt. · 2fde0890
  Guillaume Melquiond authored Apr 23, 2010
  
  2fde0890
- Removed useless theorems. · 875447d5
  Guillaume Melquiond authored Apr 23, 2010
  
  875447d5
- Simplified proofs on rounding DN and UP for generic format. · 84335f01
  Guillaume Melquiond authored Apr 23, 2010
  
  84335f01
13 Apr, 2010 7 commits
- Added theorem generic_N_pt. · ccbe9e16
  Guillaume Melquiond authored Apr 13, 2010
  
  ccbe9e16
- Added lemmas Rmult_min_distr_*. · b93c5946
  Guillaume Melquiond authored Apr 13, 2010
  
  b93c5946
- Added lemma Rmult_minus_distr_r. · cd5be868
  Guillaume Melquiond authored Apr 13, 2010
  
  cd5be868
- Added lemma Rnd_DN_UP_pt_N. · 23cf3d6e
  Guillaume Melquiond authored Apr 13, 2010
  
  23cf3d6e
- Switched Znearest from total_order_T to Rcompare. · 502358ba
  Guillaume Melquiond authored Apr 13, 2010
  
  502358ba
- Added case-friendly versions of ternary comparisons. · 4cd3fa94
  Guillaume Melquiond authored Apr 13, 2010
  
  4cd3fa94
- Generalized Znearest. · 91c934af
  Guillaume Melquiond authored Apr 13, 2010
  
  91c934af
12 Apr, 2010 3 commits
- Added two lemmas for the nearest property of ZnearestE. · 9813cd34
  Guillaume Melquiond authored Apr 12, 2010
  
  9813cd34
- Added ZnearestE function. · 7d97af76
  Guillaume Melquiond authored Apr 12, 2010
  
  7d97af76
- Replaced some Rnd_DN/UP_pt with explicit formulas for rounded values. · ae25c54d
  Guillaume Melquiond authored Apr 12, 2010
  
  ae25c54d
10 Mar, 2010 3 commits
- Used structures for storing integer rounding. · f544763b
  Guillaume Melquiond authored Mar 10, 2010
  
  f544763b
- Factored the monotony proof. · 86aae679
  Guillaume Melquiond authored Mar 10, 2010
  
  86aae679
- Proved monotony for any rounding function based on integer rounding. · bd689358
  Guillaume Melquiond authored Mar 10, 2010
  
  bd689358
05 Mar, 2010 2 commits
- Changed theorems so that they use the canonic exponent of x instead of DN(x). · 084610db
  Guillaume Melquiond authored Mar 05, 2010
  
  084610db
- Filled some proof holes. · bc990228
  Guillaume Melquiond authored Mar 05, 2010
  
  bc990228
04 Mar, 2010 8 commits
- Started a proof on computing the rounded NE value. · 40bbb808
  Guillaume Melquiond authored Mar 04, 2010
  
  40bbb808
- Modified ulp_pred_succ_pt so that it directly describes the next rounded value. · 022240d7
  Guillaume Melquiond authored Mar 04, 2010
  
  022240d7
- Renamed Z(floor/ceil)_Z to _Z2R. · 0e06838e
  Guillaume Melquiond authored Mar 04, 2010
  
  0e06838e
- Added lemma on generic formats being discrete sets. · fd490bb1
  Guillaume Melquiond authored Mar 04, 2010
  
  fd490bb1
- Made canonic floats explicit for generic format. · 5120bc45
  Guillaume Melquiond authored Mar 04, 2010
  
  5120bc45
- Added Ztrunc function. · dd74b2f2
  Guillaume Melquiond authored Mar 04, 2010
  
  dd74b2f2
- Added lemma F2R_lt_bpow. · ea71d683
  Guillaume Melquiond authored Mar 04, 2010
  
  ea71d683
- Added F2R_eq_reg. · 8f2bfea6
  Guillaume Melquiond authored Mar 04, 2010
  
  8f2bfea6
02 Mar, 2010 2 commits
- Added Rnd_NG_pt_refl. · 2f757e26
  Guillaume Melquiond authored Mar 02, 2010
  
  2f757e26
- Added theorem on truncating floats. · f92a4d94
  Guillaume Melquiond authored Mar 02, 2010
  
  f92a4d94
01 Mar, 2010 1 commit
- Added some facts about location and rounding. · ad0188af
  Guillaume Melquiond authored Mar 01, 2010
  
  ad0188af
24 Feb, 2010 4 commits
- Added splitting around rounding bounds. · c04b5ef9
  Guillaume Melquiond authored Feb 24, 2010
  
  c04b5ef9
- Generalized lemma. · a29eed78
  Guillaume Melquiond authored Feb 24, 2010
  
  a29eed78
- Added some new lemmas. Unsuccesfully tried to convert some lemmas from Pff. · 6f68b82d
  Guillaume Melquiond authored Feb 24, 2010
  
  6f68b82d
- Refactored file hierarchy. · 12ff1621
  Guillaume Melquiond authored Feb 24, 2010
  
  12ff1621
17 Feb, 2010 2 commits
- Moved format-specific theorems to their respective files. · e9f1f968
  Guillaume Melquiond authored Feb 17, 2010
  
  e9f1f968
- Removed generic NE and directly proved theorems on NE. · 6fe707a1
  Guillaume Melquiond authored Feb 17, 2010
  
  6fe707a1
10 Feb, 2010 3 commits
- Added nearest even property to FIX, FLX, and FLT. · 840b5207
  Guillaume Melquiond authored Feb 10, 2010
  
  840b5207
- Simplified proof a bit. · 6ef6c1a1
  Guillaume Melquiond authored Feb 10, 2010
  
  6ef6c1a1
- Generalized parity condition for both existence and unicity. · 4459fba8
  Guillaume Melquiond authored Feb 10, 2010
```
Generalized proofs for any generic format.
```
  4459fba8
04 Feb, 2010 1 commit
- Factored exponent equalities between FLT and FIX. · a0f1ebb4
  Guillaume Melquiond authored Feb 04, 2010
  
  a0f1ebb4