michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Commit graph

  • ce43c1cbae Fix cup symbol. In Emacs, the unicode characters cup and cap are assigned incorrectly. Leonardo de Moura 2013-08-18 18:43:31 -0700
  • a46bf357b0 Fix bug in level.cpp. Add new example Leonardo de Moura 2013-08-18 18:37:47 -0700
  • 95cfac426d Add parse_level. Fix bug at environment::is_ge Leonardo de Moura 2013-08-18 18:25:34 -0700
  • 5d609928af Add support for reading input files from the command line. Leonardo de Moura 2013-08-18 16:23:29 -0700
  • aa49eb4b0f Run examples during testing Leonardo de Moura 2013-08-18 15:51:27 -0700
  • 676ebcca3d Add parse_arrow Leonardo de Moura 2013-08-18 15:44:39 -0700
  • 4d5b65fe87 Fix bug in parser. Leonardo de Moura 2013-08-18 15:23:01 -0700
  • afd62ced87 Add parse_let Leonardo de Moura 2013-08-18 15:03:58 -0700
  • 7a9319b72e Pretty print let expressions Leonardo de Moura 2013-08-18 14:29:32 -0700
  • dc551c80dc Update .travis.osx.yml and add scripts to run doxygen and testcov on travis-ci(OSX) Soonho Kong 2013-08-18 11:22:36 -0700
  • ae523e33b4 Add parse_theorem and parse_definition Leonardo de Moura 2013-08-18 12:48:02 -0700
  • 5d2027d889 Add parse_lambda and parse_pi Leonardo de Moura 2013-08-18 12:21:11 -0700
  • 85222e13ba Add small example Leonardo de Moura 2013-08-18 10:59:59 -0700
  • 843253355b Improve parser Leonardo de Moura 2013-08-18 10:50:14 -0700
  • cdccca9316 Rename builtin operator if-then-else Leonardo de Moura 2013-08-18 10:48:38 -0700
  • 51280864cf Move '\' character to class b Leonardo de Moura 2013-08-18 10:47:13 -0700
  • 7ec7b4dce8 Fix bug in pretty printer Leonardo de Moura 2013-08-18 10:45:12 -0700
  • 18f319d00f Add more notation Leonardo de Moura 2013-08-18 10:43:55 -0700
  • 823fe6df07 Move test from lean.cpp Leonardo de Moura 2013-08-18 10:41:00 -0700
  • c82a704302 Add Lean default application. Leonardo de Moura 2013-08-18 10:37:00 -0700
  • ec83fd8093 Fix interval::acosh and add more tests on interval to improve code coverage Soonho Kong 2013-08-18 01:19:04 -0700
  • 65b4845fbc Add more tests to improve coverage. Fix bug in mpz. Leonardo de Moura 2013-08-18 00:28:26 -0700
  • ecd8eb7912 Update README.md to include instructions for tests, coverage, and doxygen Soonho Kong 2013-08-17 20:51:26 -0700
  • 3b0a7a2d96 Update src/CMakeLists.txt to include 'TESTCOV' build Soonho Kong 2013-08-17 20:37:10 -0700
  • 06f1b2a7db Add parse_expr. Add more tests. Leonardo de Moura 2013-08-17 18:35:50 -0700
  • 685aeae43a Add parser skeleton Leonardo de Moura 2013-08-17 18:13:55 -0700
  • f1961ab33f Add another pp example Leonardo de Moura 2013-08-17 12:38:32 -0700
  • 80ec48c93d Make sure formatter can be used even when associated frontend is not in scope. Leonardo de Moura 2013-08-17 12:33:19 -0700
  • 6edae938b7 Improve list iterator Leonardo de Moura 2013-08-17 11:31:36 -0700
  • a6f36ba546 Improve formatter usage. Fix bug in object printer. Leonardo de Moura 2013-08-17 11:29:43 -0700
  • 0f3af23778 Fix crash when trying to format an object created by a different frontend. Leonardo de Moura 2013-08-17 11:04:22 -0700
  • b633c866e6 Expose environment API in the frontend object. Add support for formatting objects. Leonardo de Moura 2013-08-17 10:55:42 -0700
  • c6226c6951 Fix typo Leonardo de Moura 2013-08-16 20:51:11 -0700
  • 15c1c97873 Refactor frontend pretty printer Leonardo de Moura 2013-08-16 20:39:24 -0700
  • 93ab18df71 Add context_to_lambda hack Leonardo de Moura 2013-08-16 18:59:56 -0700
  • 0fbfef8eb0 Remove sanitize_names from kernel Leonardo de Moura 2013-08-16 18:37:01 -0700
  • e792e079e2 Add formatter API Leonardo de Moura 2013-08-16 18:34:11 -0700
  • cbff5ea856 Cleanup Leonardo de Moura 2013-08-16 17:28:52 -0700
  • 111cdd4e62 Remove pretty printer from kernel. Add basic printing capability to exprlib module. Leonardo de Moura 2013-08-16 17:11:24 -0700
  • 519a290f32 Refactor kernel objects Leonardo de Moura 2013-08-16 15:09:26 -0700
  • c5cc5d1739 Optimize interval functions to reduce rounding-mode switches Soonho Kong 2013-08-16 17:05:12 -0700
  • 93475ac2eb Clean up interval check function Soonho Kong 2013-08-16 17:04:14 -0700
  • 3d8eda2239 Fix src/tests/interval/CMakeLists.txt to have different test names Soonho Kong 2013-08-16 16:57:01 -0700
  • c41b3dc4d8 Add kernel_exceptions. The idea is to avoid expression formatting in the kernel. It also allows different frontends to display the error messages is a different way. Leonardo de Moura 2013-08-16 12:51:12 -0700
  • 1038f7346e Refine initialization order. Polish Universe command pretty printer. Leonardo de Moura 2013-08-16 09:30:08 -0700
  • 4560527058 Conjunction and Disjunction are right associative. Add notation for implication. Use Isabelle precendence levels. Leonardo de Moura 2013-08-16 09:07:45 -0700
  • abab4b667a Define implies using ite operator. Rename mk_bin_op to mk_bin_rop (it is using right associativity). Add mk_bin_lop (for left assoc). Leonardo de Moura 2013-08-16 09:04:59 -0700
  • 1c30c68d2d Refine toplevel API Leonardo de Moura 2013-08-16 09:02:45 -0700
  • d002074419 Fix uninitialized variables bug Leonardo de Moura 2013-08-16 09:02:07 -0700
  • 07946f9e32 Fix bug in pretty printer Leonardo de Moura 2013-08-15 20:10:00 -0700
  • efbf3a434d Highlight assignment keyword Leonardo de Moura 2013-08-15 20:00:12 -0700
  • 43fa55723a Pretty print condensed definitions Leonardo de Moura 2013-08-15 19:56:29 -0700
  • 5ec2780321 Extend formatter with support for definitions and postulates. Leonardo de Moura 2013-08-15 19:26:49 -0700
  • 790d4a4447 Move pretty printer to frontend. Add support for mixfix pretty printing Leonardo de Moura 2013-08-15 18:54:01 -0700
  • 5395ced0e5 Improve comments Leonardo de Moura 2013-08-15 10:46:13 -0700
  • e9106f7512 Delete obsolete function continue_on_violation Leonardo de Moura 2013-08-15 10:13:48 -0700
  • d6d221b992 Move auxiliary files away from kernel Leonardo de Moura 2013-08-15 10:04:24 -0700
  • 99219f998b Rename files sets.h and maps.h to expr_sets.h and expr_maps.h Leonardo de Moura 2013-08-15 09:43:56 -0700
  • 013fa866fa Add iterator for traversing local objects (i.e., ignores objects defined in ancestor environments) Leonardo de Moura 2013-08-15 09:29:42 -0700
  • 2b7834c5fc Add methods for creating infix, prefix, postfix operators in the frontend object Leonardo de Moura 2013-08-15 08:52:10 -0700
  • 577256fedc Add highlight_keyword, highlight_builtin, highlight_command for consistent formatting Leonardo de Moura 2013-08-15 08:32:13 -0700
  • c5db989e38 Add csc, sec, cot to interval & add tests for them Soonho Kong 2013-08-15 14:38:50 -0700
  • a6f3122146 Fix cygwin error caused by the use of thread_local in numerics/float class Soonho Kong 2013-08-15 13:49:15 -0700
  • 96c4343b0c Simplify .travis.osx.yml Soonho Kong 2013-08-15 11:51:46 -0700
  • 25bfb58f17 Update interval tests to reduce compile-time Soonho Kong 2013-08-15 11:10:50 -0700
  • 7059836e21 Add more tests for float and double interval Soonho Kong 2013-08-14 23:48:55 -0700
  • f87b4394d3 Fix precision problem in interval<T>::cos Soonho Kong 2013-08-14 23:48:01 -0700
  • eb29a67395 Fix mpfp::operator^= to resolve operator overloading problem Soonho Kong 2013-08-14 23:47:36 -0700
  • 2d74ff5fe0 Cache results of the normalizer. Add example that demonstrates the exponential performance improvement. Leonardo de Moura 2013-08-14 23:18:50 -0700
  • 984c4149fa Add helper functions for creating Let expressions. Add simple type checking test for Let expressions. Leonardo de Moura 2013-08-14 22:30:12 -0700
  • da764aec14 Add more test to interval, to check inclusion property of the results Soonho Kong 2013-08-14 19:52:35 -0700
  • 0a2ac88dd1 Fix interval<T>::cosh Soonho Kong 2013-08-14 19:51:54 -0700
  • cd71218a68 Fix interval::sin and interval<tan> to pass inclusion property check Soonho Kong 2013-08-14 19:39:31 -0700
  • ce74c62226 Change interval<T>::contains to take const argument Soonho Kong 2013-08-14 16:36:07 -0700
  • a56bfe3397 Fix interval<T>::power(n) to round downward/upward when n is odd number Soonho Kong 2013-08-14 16:35:51 -0700
  • b0f2ee6de0 Add notation support to frontend object Leonardo de Moura 2013-08-14 18:16:11 -0700
  • f604be760d Add helper function for maps. Leonardo de Moura 2013-08-14 18:15:52 -0700
  • 913fd14549 Add operator== to list Leonardo de Moura 2013-08-14 16:35:04 -0700
  • 5bfb074eaf Create objects for universe variable declarations. Leonardo de Moura 2013-08-14 15:51:56 -0700
  • 285c8dafdc Display context_entry body when pretty printing contexts. Leonardo de Moura 2013-08-14 15:37:40 -0700
  • d71c36ed60 Improve sanitizer test Leonardo de Moura 2013-08-14 15:22:58 -0700
  • 23d245bb2e Sanitize context names before generating error messages. Add [[ noreturn ]] attribute to functions that always throw exceptions. Leonardo de Moura 2013-08-14 15:19:05 -0700
  • a6f0a69186 Avoid head and tail when manipulating contexts Leonardo de Moura 2013-08-14 14:42:48 -0700
  • 56305e4672 Add sanitize_names for (local) contexts Leonardo de Moura 2013-08-14 14:00:30 -0700
  • e5b8c45b3f Rename type to domain in contexts (aka telescopes). Reason: make name convention consistent with the one used for abstractions (lambdas and pis). Leonardo de Moura 2013-08-14 12:11:08 -0700
  • 338ce88ea0 Add occurs function Leonardo de Moura 2013-08-14 12:00:11 -0700
  • 38a3dfdd85 Fix interval<T>::cosh Soonho Kong 2013-08-14 15:05:22 -0700
  • eaa531bc02 Add asinh, acosh, atanh to interval Soonho Kong 2013-08-14 14:52:02 -0700
  • 43b25a0231 Add operator<(mpq, double) to mpq Soonho Kong 2013-08-14 13:45:29 -0700
  • 5a38480cf7 Remove "continue_on_violation(true);" from tests Soonho Kong 2013-08-14 13:24:18 -0700
  • 49b8bde67c Add asin, acos, atan, sinh, cosh, tanh to interval Soonho Kong 2013-08-14 12:08:24 -0700
  • 56f4050932 Add {float,double,mpfp}_interval.cpp in tests/interval Soonho Kong 2013-08-14 10:56:05 -0700
  • 840403db42 Add more test Soonho Kong 2013-08-14 00:01:29 -0700
  • 8ce6bc8050 Add tan to interval Soonho Kong 2013-08-14 00:01:23 -0700
  • 70f383eb82 Add unary minus operator overloadings to mpq & mpfp Soonho Kong 2013-08-14 00:01:03 -0700
  • d51e2e3a25 Add more test to interval Soonho Kong 2013-08-13 23:05:00 -0700
  • e0ffaed41a Fix log/exp in interval Soonho Kong 2013-08-13 23:04:55 -0700
  • 60ee5e08fb Add more test to interval Soonho Kong 2013-08-13 20:08:40 -0700
  • 548f5f069a Add fmod, sin, cos to interval<T> Soonho Kong 2013-08-13 20:08:23 -0700
  • d5f2d6b26f Fix default constructor of interval<T> to call reset method to assign 0 Soonho Kong 2013-08-13 20:07:20 -0700