max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: failing grind test cases for linarith on ordered fields (#9756)

Browse source
This commit is contained in:
Kim Morrison 2025-08-06 19:31:09 +10:00 • committed by GitHub
parent 953a1eefbb
commit dcba6dfa7e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 14 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
tests/lean/grind/algebra/linarith_field.lean Normal file
View file

@ -0,0 +1,14 @@
open Lean.Grind
variable {α : Type} [Field α] [LinearOrder α] [OrderedRing α]
example (a b : α) (h : a < b / 2) : 2 * a < b := by grind
example (a b : α) (h : a < b / 2) : a + a < b := by grind
example (a b : α) (h : a < b / 2) : 2 * a ≤ b := by grind
example (a b : α) (h : a < b / 2) : a + a ≤ b := by grind
example (a b : α) (h : a ≤ b / 2) : 2 * a ≤ b := by grind
example (a b : α) (h : a ≤ b / 2) : a + a ≤ b := by grind
example (a b : α) (_ : 0 ≤ a) (h : a ≤ b) : a / 7 ≤ b / 2 := by grind
example (a b : α) (_ : b < 0) (h : a < b) : (3/2) * a < (5/4) * b := by grind