1. 08 Mar, 2019 1 commit
  2. 07 Mar, 2019 1 commit
  3. 27 Feb, 2019 1 commit
  4. 18 Feb, 2019 1 commit
  5. 12 Feb, 2019 3 commits
  6. 08 Feb, 2019 1 commit
  7. 05 Feb, 2019 1 commit
  8. 01 Feb, 2019 1 commit
  9. 17 Jan, 2019 1 commit
    • Quentin Garchery's avatar
      hybrid eliminate_if · 5d7a985a
      Quentin Garchery authored
      we continue to use the duplicating version of eliminate_if_term for
      atomic formulas but we replace if-then-else with epsilon in Tlet and Tcase
      5d7a985a
  10. 11 Dec, 2018 1 commit
  11. 07 Dec, 2018 1 commit
  12. 06 Dec, 2018 1 commit
  13. 29 Nov, 2018 1 commit
  14. 08 Nov, 2018 1 commit
  15. 07 Nov, 2018 1 commit
  16. 30 Oct, 2018 1 commit
  17. 29 Oct, 2018 1 commit
  18. 26 Oct, 2018 1 commit
  19. 23 Oct, 2018 1 commit
  20. 16 Oct, 2018 1 commit
  21. 23 Sep, 2018 2 commits
  22. 20 Sep, 2018 1 commit
  23. 10 Sep, 2018 1 commit
  24. 05 Sep, 2018 1 commit
  25. 30 Aug, 2018 1 commit
  26. 19 Jul, 2018 3 commits
  27. 17 Jul, 2018 1 commit
    • Andrei Paskevich's avatar
      Ident: disambiguated symbolic notation · 295cacf4
      Andrei Paskevich authored
      It is possible to append an arbitary number of quote symbols
      at the end of an prefix/infix/mixfix operator:
      
                  applied form      standalone form
      
                    -' 42               (-'_)
                    x +' y              (+')
                    a[0]' <- 1          ([]'<-)
      
      Pretty-printing will use the quote symbols for disambiguation.
      
      The derived symbols can be produced by Why3 by appending
      a suffix of the form "_toto" or "'toto". These symbols can
      be parsed/printed as "(+)_toto" or "(+)'toto", respectively.
      295cacf4
  28. 21 Jun, 2018 1 commit
  29. 17 Jun, 2018 2 commits
  30. 15 Jun, 2018 2 commits
  31. 14 Jun, 2018 1 commit
  32. 06 Jun, 2018 1 commit
  33. 01 Jun, 2018 1 commit