diff --git a/examples/ex10.lean b/examples/ex10.lean deleted file mode 100644 index 29ef13d2d..000000000 --- a/examples/ex10.lean +++ /dev/null @@ -1,24 +0,0 @@ -(* Define a "fake" type to simulate the natural numbers. This is just a test. *) -Variable Natural : Type -Variable lt : Natural -> Natural -> Bool -Variable zero : Natural -Variable one : Natural -Variable two : Natural -Variable three : Natural -Infix 50 < : lt -Axiom two_lt_three : two < three -Definition vector (A : Type) (n : Natural) : Type := Pi (i : Natural) (H : i < n), A -Definition const (A : Type) (n : Natural) (d : A) : vector A n := fun (i : Natural) (H : i < n), d -Definition update (A : Type) (n : Natural) (v : vector A n) (i : Natural) (d : A) : vector A n := fun (j : Natural) (H : j < n), if A (j = i) d (v j H) -Definition select (A : Type) (n : Natural) (v : vector A n) (i : Natural) (H : i < n) : A := v i H -Definition map (A B C : Type) (n : Natural) (f : A -> B -> C) (v1 : vector A n) (v2 : vector B n) : vector C n := fun (i : Natural) (H : i < n), f (v1 i H) (v2 i H) -Show Environment -Check select Bool three (update Bool three (const Bool three false) two true) two two_lt_three -Eval select Bool three (update Bool three (const Bool three false) two true) two two_lt_three -Check select -Echo "\nmap type ---> " -Check map -Echo "\nmap normal form --> " -Eval map -Echo "\nupdate normal form --> " -Eval update diff --git a/examples/ex2.lean b/examples/ex2.lean deleted file mode 100644 index d49699638..000000000 --- a/examples/ex2.lean +++ /dev/null @@ -1,6 +0,0 @@ -Check fun x : Bool, x -Show fun x y : Bool, x -Show fun (A : Type) (x y : A), x = y -Check fun (A : Type) (x y : A), x = y -Check Pi (A B : Type), Type -Show Pi (A B : Type), A = B \ No newline at end of file diff --git a/src/kernel/arith/arith.cpp b/src/kernel/arith/arith.cpp index 6754c0dc5..b8d258943 100644 --- a/src/kernel/arith/arith.cpp +++ b/src/kernel/arith/arith.cpp @@ -19,8 +19,8 @@ public: virtual expr get_type() const { return Type(); } virtual bool normalize(unsigned num_args, expr const * args, expr & r) const { return false; } virtual bool operator==(value const & other) const { return other.kind() == kind(); } - virtual void display(std::ostream & out) const { out << "int"; } - virtual format pp() const { return format("int"); } + virtual void display(std::ostream & out) const { out << "Int"; } + virtual format pp() const { return format("Int"); } virtual unsigned hash() const { return 41; } }; diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index a0989816a..913b4526c 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -2,23 +2,6 @@ configure_file("${LEAN_SOURCE_DIR}/shell/version.h.in" "${LEAN_BINARY_DIR}/versi include_directories("${LEAN_BINARY_DIR}") add_executable(lean lean.cpp) target_link_libraries(lean ${EXTRA_LIBS}) -add_test(lean1 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex1.lean") -add_test(lean2 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex2.lean") -add_test(lean3 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex3.lean") -add_test(lean4 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex4.lean") -add_test(lean5 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex5.lean") -add_test(lean6 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex6.lean") -add_test(lean7 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex7.lean") -add_test(lean8 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex8.lean") -add_test(lean9 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex9.lean") -add_test(lean10 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex10.lean") -add_test(lean11 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex11.lean") -add_test(lean12 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex12.lean") -add_test(lean13 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex13.lean") -add_test(lean14 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex14.lean") -add_test(lean15 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex15.lean") -add_test(lean16 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex16.lean") -add_test(lean17 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex17.lean") add_test(NAME leantests WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean" COMMAND "./test.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean") diff --git a/examples/deep.lean b/tests/lean/deep.lean similarity index 100% rename from examples/deep.lean rename to tests/lean/deep.lean diff --git a/tests/lean/deep.lean.expected.out b/tests/lean/deep.lean.expected.out new file mode 100644 index 000000000..cc164c66c --- /dev/null +++ b/tests/lean/deep.lean.expected.out @@ -0,0 +1,7 @@ + Defined: f1 + Defined: f2 + Defined: f3 + Assumed: f + Set option: pp::width + Set option: lean::pp::max_depth +f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (…)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) diff --git a/tests/lean/tst1.lean b/tests/lean/tst1.lean new file mode 100644 index 000000000..28a8455e5 --- /dev/null +++ b/tests/lean/tst1.lean @@ -0,0 +1,26 @@ +(* Define a "fake" type to simulate the natural numbers. This is just a test. *) +Variable N : Type +Variable lt : N -> N -> Bool +Variable zero : N +Variable one : N +Variable two : N +Variable three : N +Infix 50 < : lt +Axiom two_lt_three : two < three +Definition vector (A : Type) (n : N) : Type := Pi (i : N) (H : i < n), A +Definition const {A : Type} (n : N) (d : A) : vector A n := fun (i : N) (H : i < n), d +Definition update {A : Type} {n : N} (v : vector A n) (i : N) (d : A) : vector A n := fun (j : N) (H : j < n), if A (j = i) d (v j H) +Definition select {A : Type} {n : N} (v : vector A n) (i : N) (H : i < n) : A := v i H +Definition map {A B C : Type} {n : N} (f : A -> B -> C) (v1 : vector A n) (v2 : vector B n) : vector C n := fun (i : N) (H : i < n), f (v1 i H) (v2 i H) +Show Environment 10 +Check select (update (const three false) two true) two two_lt_three +Eval select (update (const three false) two true) two two_lt_three +Check update (const three false) two true +Echo "\n--------" +Check select::explicit +Echo "\nmap type ---> " +Check map::explicit +Echo "\nmap normal form --> " +Eval map::explicit +Echo "\nupdate normal form --> " +Eval update::explicit diff --git a/tests/lean/tst1.lean.expected.out b/tests/lean/tst1.lean.expected.out new file mode 100644 index 000000000..0723a3783 --- /dev/null +++ b/tests/lean/tst1.lean.expected.out @@ -0,0 +1,47 @@ + Assumed: N + Assumed: lt + Assumed: zero + Assumed: one + Assumed: two + Assumed: three + Assumed: two_lt_three + Defined: vector + Defined: const + Defined: update + Defined: select + Defined: map +Axiom two_lt_three : two < three +Definition vector (A : Type) (n : N) : Type := Π (i : N) (H : i < n), A +Definition const {A : Type} (n : N) (d : A) : vector A n := λ (i : N) (H : i < n), d +Definition const::explicit (A : Type) (n : N) (d : A) : vector A n := const n d +Definition update {A : Type} {n : N} (v : vector A n) (i : N) (d : A) : vector A n := + λ (j : N) (H : j < n), if A (j = i) d (v j H) +Definition update::explicit (A : Type) (n : N) (v : vector A n) (i : N) (d : A) : vector A n := update v i d +Definition select {A : Type} {n : N} (v : vector A n) (i : N) (H : i < n) : A := v i H +Definition select::explicit (A : Type) (n : N) (v : vector A n) (i : N) (H : i < n) : A := select v i H +Definition map {A B C : Type} {n : N} (f : A → B → C) (v1 : vector A n) (v2 : vector B n) : vector C n := + λ (i : N) (H : i < n), f (v1 i H) (v2 i H) +Definition map::explicit (A B C : Type) (n : N) (f : A → B → C) (v1 : vector A n) (v2 : vector B n) : vector C n := + map f v1 v2 +Bool +⊤ +vector Bool three + +-------- +Π (A : Type) (n : N) (v : vector A n) (i : N) (H : i < n), A + +map type ---> +Π (A B C : Type) (n : N) (f : A → B → C) (v1 : vector A n) (v2 : vector B n), vector C n + +map normal form --> +λ (A B C : Type) + (n : N) + (f : A → B → C) + (v1 : Π (i : N) (H : i < n), A) + (v2 : Π (i : N) (H : i < n), B) + (i : N) + (H : i < n), + f (v1 i H) (v2 i H) + +update normal form --> +λ (A : Type) (n : N) (v : Π (i : N) (H : i < n), A) (i : N) (d : A) (j : N) (H : j < n), ite A (j = i) d (v j H) diff --git a/examples/ex1.lean b/tests/lean/tst10.lean similarity index 100% rename from examples/ex1.lean rename to tests/lean/tst10.lean diff --git a/tests/lean/tst10.lean.expected.out b/tests/lean/tst10.lean.expected.out new file mode 100644 index 000000000..e985776c6 --- /dev/null +++ b/tests/lean/tst10.lean.expected.out @@ -0,0 +1,22 @@ + Assumed: a + Assumed: b +a ∧ b +a ∧ b ∧ a +a ∧ b +a ∧ b +a ∧ b +a ∧ b +a ∨ b +a ∨ b +a ∨ b +a ∨ b +a ∨ a ∨ b +a ⇒ b ⇒ a +Bool +ite Bool a a ⊤ +a + Assumed: H1 + Assumed: H2 +Π (a b : Bool) (H1 : a ⇒ b) (H2 : a), b +MP H2 H1 +b diff --git a/examples/ex3.lean b/tests/lean/tst11.lean similarity index 100% rename from examples/ex3.lean rename to tests/lean/tst11.lean diff --git a/tests/lean/tst11.lean.expected.out b/tests/lean/tst11.lean.expected.out new file mode 100644 index 000000000..264631a6d --- /dev/null +++ b/tests/lean/tst11.lean.expected.out @@ -0,0 +1,10 @@ + Defined: xor +⊤ ⊕ ⊥ +⊥ +⊤ + Assumed: a +a ⊕ a ⊕ a +Π (A : Type u) (a b : A) (P : A → Bool) (H1 : P a) (H2 : a = b), P b + Proved: EM2 +Π a : Bool, a ∨ ¬ a +a ∨ ¬ a diff --git a/examples/ex4.lean b/tests/lean/tst12.lean similarity index 100% rename from examples/ex4.lean rename to tests/lean/tst12.lean diff --git a/tests/lean/tst12.lean.expected.out b/tests/lean/tst12.lean.expected.out new file mode 100644 index 000000000..5f45439b1 --- /dev/null +++ b/tests/lean/tst12.lean.expected.out @@ -0,0 +1,7 @@ +λ x y : Bool, x ∧ y +let x := ⊤, + y := ⊤, + z := x ∧ y, + f := λ arg1 arg2 : Bool, arg1 ∧ arg2 ⇔ arg2 ∧ arg1 ⇔ arg1 ∨ arg2 ∨ arg2 +in (f x y) ∨ z +⊤ diff --git a/examples/ex5.lean b/tests/lean/tst13.lean similarity index 100% rename from examples/ex5.lean rename to tests/lean/tst13.lean diff --git a/tests/lean/tst13.lean.expected.out b/tests/lean/tst13.lean.expected.out new file mode 100644 index 000000000..a879ffc90 --- /dev/null +++ b/tests/lean/tst13.lean.expected.out @@ -0,0 +1,2 @@ +λ x x : Bool, x +let x := ⊤, y := ⊤, z := x ∧ y, f := λ x y : Bool, x ∧ y ⇔ y ∧ x ⇔ x ∨ y ∨ y in (f x y) ∨ z diff --git a/examples/ex6.lean b/tests/lean/tst14.lean similarity index 100% rename from examples/ex6.lean rename to tests/lean/tst14.lean diff --git a/tests/lean/tst14.lean.expected.out b/tests/lean/tst14.lean.expected.out new file mode 100644 index 000000000..ae8fd1a7a --- /dev/null +++ b/tests/lean/tst14.lean.expected.out @@ -0,0 +1,5 @@ +Int → Int → Int + Assumed: f +f 0 +Int → Int +Int diff --git a/examples/ex7.lean b/tests/lean/tst15.lean similarity index 100% rename from examples/ex7.lean rename to tests/lean/tst15.lean diff --git a/tests/lean/tst15.lean.expected.out b/tests/lean/tst15.lean.expected.out new file mode 100644 index 000000000..d20403132 --- /dev/null +++ b/tests/lean/tst15.lean.expected.out @@ -0,0 +1,20 @@ + Assumed: x +Type u+3 ⊔ m+2 ⊔ 3 + Assumed: f +Type u+10 → Type +Type +Type 5 +Type u+3 ⊔ m+2 ⊔ 3 +Type u+1 ⊔ m+1 +Type u+3 +Type u+4 +Type u+1 ⊔ m+1 +Type u+1 ⊔ m+1 ⊔ 4 +Type u+1 ⊔ m ⊔ 3 +Type u+2 ⊔ m+1 ⊔ 4 +Type u → Type 5 +Type u+1 ⊔ 6 +Type m+1 ⊔ 4 ⊔ u+6 +Type m ⊔ 3 → Type u → Type 5 +Type m+1 ⊔ 6 ⊔ u+1 +Type u diff --git a/examples/ex8.lean b/tests/lean/tst16.lean similarity index 100% rename from examples/ex8.lean rename to tests/lean/tst16.lean diff --git a/tests/lean/tst16.lean.expected.out b/tests/lean/tst16.lean.expected.out new file mode 100644 index 000000000..e2062caa3 --- /dev/null +++ b/tests/lean/tst16.lean.expected.out @@ -0,0 +1,15 @@ + Assumed: f +∀ a b : Type, (f a) = (f b) + Assumed: g +∀ (a b : Type) (c : Bool), g c ((f a) = (f b)) +∃ (a b : Type) (c : Bool), g c ((f a) = (f b)) +∀ (a b : Type) (c : Bool), (g c (f a)) = (f b) ⇒ (f a) +Bool +∀ (a b : Type) (c : Bool), g c ((f a) = (f b)) +∀ a b : Type, (f a) = (f b) +∃ a b : Type, (f a) = (f b) ∧ (f a) +∃ a b : Type, (f a) = (f b) ∨ (f b) + Assumed: a +(f a) ∨ (f a) +(f a) = a ∨ (f a) +(f a) = a ∧ (f a) diff --git a/examples/ex9.lean b/tests/lean/tst17.lean similarity index 100% rename from examples/ex9.lean rename to tests/lean/tst17.lean diff --git a/tests/lean/tst17.lean.expected.out b/tests/lean/tst17.lean.expected.out new file mode 100644 index 000000000..411fc2eea --- /dev/null +++ b/tests/lean/tst17.lean.expected.out @@ -0,0 +1,8 @@ + Assumed: f + Assumed: g +∀ a b : Type, ∃ c : Type, (g a b) = (f c) +Bool +(λ a : Type, + (λ b : Type, ite Bool ((λ x : Type, ite Bool ((g a b) = (f x)) ⊥ ⊤) = (λ x : Type, ⊤)) ⊥ ⊤) = + (λ x : Type, ⊤)) = +(λ x : Type, ⊤) diff --git a/examples/ex11.lean b/tests/lean/tst2.lean similarity index 89% rename from examples/ex11.lean rename to tests/lean/tst2.lean index da2bab733..595725f49 100644 --- a/examples/ex11.lean +++ b/tests/lean/tst2.lean @@ -5,8 +5,7 @@ Show a/\b Set lean::pp::notation false Show Options Show a/\b -Show Environment 5 +Show Environment 2 Set lean::pp::notation true Show Options Show a/\b - diff --git a/tests/lean/tst2.lean.expected.out b/tests/lean/tst2.lean.expected.out new file mode 100644 index 000000000..f362feaf1 --- /dev/null +++ b/tests/lean/tst2.lean.expected.out @@ -0,0 +1,12 @@ +⟨⟩ + Assumed: a + Assumed: b +a ∧ b + Set option: lean::pp::notation +⟨lean::pp::notation ↦ false⟩ +and a b +Variable a : Bool +Variable b : Bool + Set option: lean::pp::notation +⟨lean::pp::notation ↦ true⟩ +a ∧ b diff --git a/examples/ex12.lean b/tests/lean/tst3.lean similarity index 99% rename from examples/ex12.lean rename to tests/lean/tst3.lean index 1a17cea84..a7f68b0cd 100644 --- a/examples/ex12.lean +++ b/tests/lean/tst3.lean @@ -1,5 +1,3 @@ - - Set lean::parser::verbose false. Notation 10 if _ then _ : implies. Show Environment 1. diff --git a/tests/lean/tst3.lean.expected.out b/tests/lean/tst3.lean.expected.out new file mode 100644 index 000000000..bbc747917 --- /dev/null +++ b/tests/lean/tst3.lean.expected.out @@ -0,0 +1,25 @@ +Notation 10 if _ then _ : implies +if ⊤ then ⊥ +if ⊤ then (if a then ⊥) +implies true (implies a false) +Notation 100 _ |- _ ; _ : f +f c d e +c |- d ; e +(a !) ! +fact (fact a) +[ c ; d ] +[ c ; ([ d ; e ]) ] +g c (g d e) +Notation 40 _ << _ end : h +d << e end +[ c ; d << e end ] +g c (h d e) +c ** d ++ e ** c +p1 ∨ p2 ∧ p3 +r (s c d) (s e c) +or p1 (and p2 p3) +c = d ∨ d = c +¬ p1 ∨ p2 +p1 ∧ p3 ∨ p2 ∧ p3 +or (not p1) p2 +or (and p1 p3) (and p2 p3) diff --git a/examples/ex13.lean b/tests/lean/tst4.lean similarity index 99% rename from examples/ex13.lean rename to tests/lean/tst4.lean index 3fc0040ef..aa5236d00 100644 --- a/examples/ex13.lean +++ b/tests/lean/tst4.lean @@ -1,4 +1,3 @@ - Variable f {A : Type} (a b : A) : A Variable N : Type Variable n1 : N @@ -20,5 +19,3 @@ Axiom H1 : a = b && b = c Theorem Pr : (g a) = (g c) := Congr (Refl g) (Trans (Conjunct1 H1) (Conjunct2 H1)) Show Environment 2 - - diff --git a/tests/lean/tst4.lean.expected.out b/tests/lean/tst4.lean.expected.out new file mode 100644 index 000000000..494c83863 --- /dev/null +++ b/tests/lean/tst4.lean.expected.out @@ -0,0 +1,28 @@ + Assumed: f + Assumed: N + Assumed: n1 + Assumed: n2 + Set option: lean::pp::implicit +f::explicit N n1 n2 +f::explicit ((N → N) → N → N) (λ x : N → N, x) (λ y : N → N, y) + Assumed: EqNice +EqNice::explicit N n1 n2 +N +Π (A : Type u) (B : A → Type u) (f g : Π x : A, B x) (a b : A) (H1 : f = g) (H2 : a = b), (f a) = (g b) +f::explicit N n1 n2 + Assumed: a + Assumed: b + Assumed: c + Assumed: g + Assumed: H1 + Proved: Pr +Axiom H1 : a = b ∧ b = c +Theorem Pr : (g a) = (g c) := + let κ::1 := Trans::explicit + N + a + b + c + (Conjunct1::explicit (a = b) (b = c) H1) + (Conjunct2::explicit (a = b) (b = c) H1) + in Congr::explicit N (λ x : N, N) g g a c (Refl::explicit (N → N) g) κ::1 diff --git a/examples/ex14.lean b/tests/lean/tst5.lean similarity index 100% rename from examples/ex14.lean rename to tests/lean/tst5.lean diff --git a/tests/lean/tst5.lean.expected.out b/tests/lean/tst5.lean.expected.out new file mode 100644 index 000000000..26e2ec5f0 --- /dev/null +++ b/tests/lean/tst5.lean.expected.out @@ -0,0 +1,9 @@ + Assumed: N + Assumed: a + Assumed: b +a ≃ b +Bool + Set option: lean::pp::implicit +heq::explicit N a b +heq::explicit Type 2 Type 1 Type 1 +heq::explicit Bool ⊤ ⊥ diff --git a/examples/ex15.lean b/tests/lean/tst6.lean similarity index 100% rename from examples/ex15.lean rename to tests/lean/tst6.lean diff --git a/tests/lean/tst6.lean.expected.out b/tests/lean/tst6.lean.expected.out new file mode 100644 index 000000000..a04b66c42 --- /dev/null +++ b/tests/lean/tst6.lean.expected.out @@ -0,0 +1,106 @@ + Assumed: N + Assumed: h + Proved: CongrH + Set option: lean::pp::implicit +Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := + Congr::explicit + N + (λ x : N, N) + (h a1) + (h b1) + a2 + b2 + (Congr::explicit N (λ x : N, N → N) h h a1 b1 (Refl::explicit (N → N → N) h) H1) + H2 +Theorem CongrH::explicit (a1 a2 b1 b2 : N) (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := + CongrH::explicit a1 a2 b1 b2 H1 H2 + Set option: lean::pp::implicit +Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := Congr (Congr (Refl h) H1) H2 +Theorem CongrH::explicit (a1 a2 b1 b2 : N) (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := CongrH H1 H2 + Proved: Example1 + Set option: lean::pp::implicit +Theorem Example1 (a b c d : N) (H : a = b ∧ b = c ∨ a = d ∧ d = c) : (h a b) = (h c b) := + DisjCases::explicit + (a = b ∧ b = c) + (a = d ∧ d = c) + ((h a b) = (h c b)) + H + (λ H1 : a = b ∧ b = c, + CongrH::explicit + a + b + c + b + (Trans::explicit + N + a + b + c + (Conjunct1::explicit (a = b) (b = c) H1) + (Conjunct2::explicit (a = b) (b = c) H1)) + (Refl::explicit N b)) + (λ H1 : a = d ∧ d = c, + CongrH::explicit + a + b + c + b + (Trans::explicit + N + a + d + c + (Conjunct1::explicit (a = d) (d = c) H1) + (Conjunct2::explicit (a = d) (d = c) H1)) + (Refl::explicit N b)) + Proved: Example2 + Set option: lean::pp::implicit +Theorem Example2 (a b c d : N) (H : a = b ∧ b = c ∨ a = d ∧ d = c) : (h a b) = (h c b) := + DisjCases::explicit + (a = b ∧ b = c) + (a = d ∧ d = c) + ((h a b) = (h c b)) + H + (λ H1 : a = b ∧ b = c, + CongrH::explicit + a + b + c + b + (Trans::explicit + N + a + b + c + (Conjunct1::explicit (a = b) (b = c) H1) + (Conjunct2::explicit (a = b) (b = c) H1)) + (Refl::explicit N b)) + (λ H1 : a = d ∧ d = c, + CongrH::explicit + a + b + c + b + (Trans::explicit + N + a + d + c + (Conjunct1::explicit (a = d) (d = c) H1) + (Conjunct2::explicit (a = d) (d = c) H1)) + (Refl::explicit N b)) + Proved: Example3 + Set option: lean::pp::implicit +Theorem Example3 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : (h a b) = (h c b) := + DisjCases + H + (λ H1 : a = b ∧ b = e ∧ b = c, CongrH (Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1))) (Refl b)) + (λ H1 : a = d ∧ d = c, CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b)) + Proved: Example4 + Set option: lean::pp::implicit +Theorem Example4 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : (h a c) = (h c a) := + DisjCases + H + (λ H1 : a = b ∧ b = e ∧ b = c, + let AeqC := Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1)) in CongrH AeqC (Symm AeqC)) + (λ H1 : a = d ∧ d = c, let AeqC := Trans (Conjunct1 H1) (Conjunct2 H1) in CongrH AeqC (Symm AeqC)) diff --git a/examples/ex16.lean b/tests/lean/tst7.lean similarity index 91% rename from examples/ex16.lean rename to tests/lean/tst7.lean index 1c52b7717..d896e8ab3 100644 --- a/examples/ex16.lean +++ b/tests/lean/tst7.lean @@ -1,7 +1,7 @@ Variable f : Pi (A : Type), A -> Bool Show fun (A B : Type) (a : _), f B a (* The following one should produce an error *) -(* Show fun (A : Type) (a : _) (B : Type), f B a *) +Show fun (A : Type) (a : _) (B : Type), f B a Variable myeq : Pi (A : Type u), A -> A -> Bool Show myeq _ (fun (A : Type) (a : _), a) (fun (B : Type) (b : B), b) diff --git a/tests/lean/tst7.lean.expected.out b/tests/lean/tst7.lean.expected.out new file mode 100644 index 000000000..882ccb075 --- /dev/null +++ b/tests/lean/tst7.lean.expected.out @@ -0,0 +1,14 @@ + Assumed: f +λ (A B : Type) (a : B), f B a +Error (line: 4, pos: 40) application type mismatch during term elaboration at term + f B a +Elaborator state + ?M0 := [unassigned] + ?M1 := [unassigned] + #0 ≈ lift:0:0 ?M0 + Assumed: myeq +myeq (Π (A : Type) (a : A), A) (λ (A : Type) (a : A), a) (λ (B : Type) (b : B), b) +Bool + Assumed: R + Assumed: h +Bool → (Π (f1 g1 : Π A : Type, R A) (G : Π A : Type, myeq (R A) (f1 A) (g1 A)), Bool) diff --git a/examples/ex17.lean b/tests/lean/tst8.lean similarity index 100% rename from examples/ex17.lean rename to tests/lean/tst8.lean diff --git a/tests/lean/tst8.lean.expected.out b/tests/lean/tst8.lean.expected.out new file mode 100644 index 000000000..9821726c6 --- /dev/null +++ b/tests/lean/tst8.lean.expected.out @@ -0,0 +1,3 @@ +Π (A : Type) (a : A), A + Assumed: g + Defined: f diff --git a/tests/lean/tst9.lean b/tests/lean/tst9.lean new file mode 100644 index 000000000..89f5efc9b --- /dev/null +++ b/tests/lean/tst9.lean @@ -0,0 +1,5 @@ +Variable f : Pi A : Type, A -> A -> A +Variable N : Type +Variable g : N -> N -> Bool +Variable a : N +Check g true (f _ a a) diff --git a/tests/lean/tst9.lean.expected.out b/tests/lean/tst9.lean.expected.out new file mode 100644 index 000000000..dc239b5e8 --- /dev/null +++ b/tests/lean/tst9.lean.expected.out @@ -0,0 +1,10 @@ + Assumed: f + Assumed: N + Assumed: g + Assumed: a +Error (line: 5, pos: 6) type mismatch at application argument 1 of + g ⊤ (f N a a) +expected type + N +given type + Bool