Commits · f7db94c9ad5db9dcb03146791d3d6b00a827f53c · Why3 / why3

02 May, 2014 10 commits
- bigInt: remove leading zeros · f7db94c9
  MARCHE Claude authored Apr 26, 2014
  
  f7db94c9
- bigInt: better test · 80631220
  MARCHE Claude authored Apr 26, 2014
  
  80631220
- bigInt: javascript · a70ac5c1
  MARCHE Claude authored Apr 26, 2014
  
  a70ac5c1
- bigInt: Z.add proved · 1aa814f0
  MARCHE Claude authored Apr 26, 2014
  
  1aa814f0
- bigInt.N.add: fully proved · a6917e6b
  MARCHE Claude authored Apr 26, 2014 and MARCHE Claude committed May 02, 2014
  
  a6917e6b
- bigInt.add: in progress · fd307916
  MARCHE Claude authored Apr 26, 2014 and MARCHE Claude committed May 02, 2014
  
  fd307916
- bigInt: attempt to prove add · a403809b
  MARCHE Claude authored Apr 26, 2014 and MARCHE Claude committed May 02, 2014
  
  a403809b
- Merge remote-tracking branch 'origin/clone_val' · bab7500c
  Andrei Paskevich authored May 02, 2014
  
  bab7500c
- AVL example: cleanup+alpha-renaming · 68d0207b
  Martin Clochard authored May 02, 2014
  
  68d0207b
- fixed session for example Defunctionalization · 836d876d
  MARCHE Claude authored May 02, 2014
  
  836d876d
30 Apr, 2014 2 commits
- AVL example: cleanup · 32b418b9
  Martin Clochard authored Apr 30, 2014
  
  32b418b9
- defunctionalization: simplified proofs · 8d5de50b
  Jean-Christophe Filliâtre authored Apr 30, 2014
  
  8d5de50b
29 Apr, 2014 4 commits
- updated proof session · 05437650
  Jean-Christophe Filliâtre authored Apr 29, 2014
  
  05437650
- why3lang.sty: added a keyword · 389fa675
  Jean-Christophe Filliâtre authored Apr 29, 2014
  
  389fa675
- inverse_in_place: fixed session · a13e2d2a
  MARCHE Claude authored Apr 29, 2014
  
  a13e2d2a
- defunctionalization, small details · 749bd595
  MARCHE Claude authored Apr 29, 2014
  
  749bd595
27 Apr, 2014 1 commit
- reverted merge mistake · 697a3bc3
  MARCHE Claude authored Apr 27, 2014
  
  697a3bc3
26 Apr, 2014 6 commits
- AVL example: added an implementation of priority queues. · 29086d27
  Martin Clochard authored Apr 26, 2014
  
  29086d27
- solved merged conflicts · c08f38e3
  MARCHE Claude authored Apr 26, 2014
  
  c08f38e3
- implementation of bigInts in Why3 · b4711106
  MARCHE Claude authored Apr 26, 2014
  
  b4711106
- More on io.mlw · 74f28874
  MARCHE Claude authored Apr 26, 2014
  
  74f28874
- new example (in progress): linear probing · b0092599
  Jean-Christophe Filliâtre authored Apr 25, 2014
  
  b0092599
- added and ignored files · 9f6ebf75
  MARCHE Claude authored Apr 26, 2014
  
  9f6ebf75
25 Apr, 2014 4 commits
- AVL example with cached values from monoid. · d17784c6
  Martin Clochard authored Apr 25, 2014
  
  d17784c6
- replay obsolete sessions · a0279278
  MARCHE Claude authored Apr 25, 2014
  
  a0279278
- cleaning up · 7fdb671e
  Jean-Christophe Filliâtre authored Apr 25, 2014
  
  7fdb671e
- euler001: update session · 919272de
  MARCHE Claude authored Apr 25, 2014
  
  919272de
24 Apr, 2014 2 commits
- gitignore · 748dc861
  MARCHE Claude authored Apr 25, 2014
  
  748dc861
- Extraction of VSTTE12_Combinators to Javascript · dd28dd61
  MARCHE Claude authored Apr 25, 2014
  
  dd28dd61
23 Apr, 2014 5 commits
- Factorize most of BigInt nums versus zarith · c67a3b49
  MARCHE Claude authored Apr 24, 2014
  
  c67a3b49
- Attempt to add a module for Input/Output · 0dbc9ed9
  MARCHE Claude authored Apr 24, 2014
  
  0dbc9ed9
- coincidence_count: simpler proof · b618fbf3
  Jean-Christophe Filliâtre authored Apr 23, 2014
  
  b618fbf3
- support for more gappa versions · c95afb9c
  MARCHE Claude authored Apr 23, 2014
  
  c95afb9c
- updated proof sessions · 31b4c6da
  Jean-Christophe Filliâtre authored Apr 23, 2014
  
  31b4c6da
22 Apr, 2014 2 commits
- new example coincindence_count (cleaned up) · 56fd5d13
  Jean-Christophe Filliâtre authored Apr 22, 2014
  
  56fd5d13
- new example coincindence_count · 9d00853c
  Jean-Christophe Filliâtre authored Apr 22, 2014
  
  9d00853c
18 Apr, 2014 1 commit
- Fix hashing so that the accumulator is multiplied rather than just summed. · a42f2345
  Guillaume Melquiond authored Apr 18, 2014
  
  a42f2345
17 Apr, 2014 1 commit
- AVL example: added set-theoretic functions · 036bdfd7
  Martin Clochard authored Apr 17, 2014
  
  036bdfd7
16 Apr, 2014 1 commit
- defunctionalization: add a variant with algebraic variant · a0f563cc
  Andrei Paskevich authored Apr 17, 2014
```
14 lines instead of 23 for the termination proofs
```
  a0f563cc
15 Apr, 2014 1 commit
- Avl example: add cardinal to associative structures. · a2b7347f
  Martin Clochard authored Apr 15, 2014
  
  a2b7347f