1. 09 Sep, 2014 4 commits
  2. 08 Sep, 2014 1 commit
  3. 07 Sep, 2014 1 commit
  4. 05 Sep, 2014 2 commits
  5. 04 Sep, 2014 4 commits
  6. 03 Sep, 2014 1 commit
  7. 02 Sep, 2014 1 commit
  8. 25 Aug, 2014 1 commit
  9. 20 Aug, 2014 8 commits
  10. 19 Aug, 2014 7 commits
  11. 18 Aug, 2014 2 commits
  12. 11 Jul, 2014 1 commit
    • Martin Clochard's avatar
      Hack to prevent eval-match from decomposing quantified records · 698ca990
      Martin Clochard authored
        This is to prevent quantified records from being decomposed by
        eval_match. e.g, assert { forall x:t. ... } was previously
        transformed to assert { forall x1:t1, x2:t2, x3:t3. ... } if x was
        a record type with fields x1,x2,x3. This changed the
        instantiation pattern, which could be harmful.
      698ca990
  13. 14 Mar, 2014 1 commit
  14. 16 Feb, 2014 1 commit
  15. 12 Feb, 2014 1 commit
  16. 04 Feb, 2014 1 commit
  17. 20 Jan, 2014 1 commit
    • Andrei Paskevich's avatar
      "eliminate_epsilon" added in drivers · 9c20cd7c
      Andrei Paskevich authored
      Currently, the builtin theory why3.HighOrd (or just HighOrd) must
      be explicitly "use"-d. However, the type (HighOrd.func 'a 'b) can
      be written ('a -> 'b), and the type (HighOrd.pred 'a) can be written
      ('a -> bool), and the application operation (HighOrd.(@)) can be
      written as the usual juxtaposition. Thus, normally, you do not have
      to write the qualifiers. The builtin theory why3.Bool (or just Bool)
      is needed for "bool". The names "HighOrd", "func", "pred", and "(@)"
      are not yet fixed and may change.
      
      "eliminate_epsilon" tries to be smart when a lambda (or some other
      comprehension form) occurs under equality or at the top of a definition.
      We could go even further and replace (\ x . t) s with t[x <- s], without
      lifting the lambda. I'm not sure it's worth it: we rarely write redexes
      manually. They can and will appear through inlining, though.
      
      Anyone who wants to construct epsilon-terms directly using the API
      should remember that these are not Hilbert's epsilons: by writing
      an epsilon term, you postulate the existence (though not necessarily
      uniqueness) of the described object, and "eliminate_epsilon" will
      happily convert it to an axiom expressing this existence. We only
      use epsilons to write comprehensions whose soundness is guaranteed
      by a background theory, e.g. lambda-calculus.
      9c20cd7c
  18. 18 Jan, 2014 1 commit
  19. 14 Jan, 2014 1 commit