From abdd784729bc55ccde51726221adcb8d90477932 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 9 Sep 2014 14:13:35 -0700 Subject: [PATCH] feat(shell): start 'lean --server' with 'pp.beta = true' --- src/shell/lean.cpp | 1 + tests/lean/run/ppbeta.lean | 10 ++++++++++ 2 files changed, 11 insertions(+) create mode 100644 tests/lean/run/ppbeta.lean diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 63c24f37a..9eca80e33 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -333,6 +333,7 @@ int main(int argc, char ** argv) { } if (ok && server && default_k == input_kind::Lean) { signal(SIGINT, on_ctrl_c); + ios.set_option(lean::name("pp", "beta"), true); lean::server Sv(env, ios, num_threads); if (!Sv(std::cin)) ok = false; diff --git a/tests/lean/run/ppbeta.lean b/tests/lean/run/ppbeta.lean new file mode 100644 index 000000000..c7a905fb2 --- /dev/null +++ b/tests/lean/run/ppbeta.lean @@ -0,0 +1,10 @@ +import data.int +open [coercions] int +open [coercions] nat + +definition lt (a b : int) := int.le (int.add a 1) b +infix `<` := lt +infixl `+`:65 := int.add + +theorem lt_add_succ2 (a : int) (n : nat) : a < a + nat.succ n := +int.le_intro (show a + 1 + n = a + nat.succ n, from sorry)