fixes

leanprover-community · Dec 22, 2023 · ea3474d · ea3474d
1 parent d6b392a
commit ea3474d
Show file tree

Hide file tree

Showing 3 changed files with 19 additions and 0 deletions.
diff --git a/test/Mathlib/ReplMathlibTests.lean b/test/Mathlib/ReplMathlibTests.lean
@@ -0,0 +1 @@
+import Mathlib
diff --git a/test/Mathlib/lakefile.lean b/test/Mathlib/lakefile.lean
@@ -5,5 +5,7 @@ package «repl-mathlib-tests» where
   -- add package configuration options here
   require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "master"
 
+@[default_target]
 lean_lib «ReplMathlibTests» where
+  globs := #[.submodules `test]
   -- add library configuration options here
diff --git a/test/Mathlib/test/H20231214.lean b/test/Mathlib/test/H20231214.lean
@@ -3,6 +3,22 @@ open Real
 open Nat
 open BigOperators
 
+/--
+error: type mismatch
+  h₀ x
+has type
+  p x = 2 - x ^ 2 : Prop
+but is expected to have type
+  p x = 6 / x * p x : Prop
+---
+error: unsolved goals
+p q : ℝ → ℝ
+h₀ : ∀ (x : ℝ), p x = 2 - x ^ 2
+h₁ : ∀ (x : ℝ), x ≠ 0 → q x = 6 / x
+hQ : ∀ (x : ℝ), p x = 6 / x
+⊢ p (q 2) = -7
+-/
+#guard_msgs in
 theorem mathd_algebra_35
   (p q : ℝ → ℝ)
   (h₀ : ∀ x, p x = 2 - x^2)