mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
37f10435a9
This PR changes the way the linting for `linter.unusedSimpArgs` gets the value from the environment. This is achieved by using the appropriate helper functions defined in `Lean.Linter.Basic`. The following now compiles without warning ```lean4 set_option linter.all false in example : True := by simp [False] ``` Fixes #12559
7 lines
423 B
Plaintext
7 lines
423 B
Plaintext
theorem ex₂ : ∀ (x₁ x₂ x₃ x₄ : Nat), x₁ + x₂ + (x₃ + x₄) = x₃ + x₁ + x₂ + x₄ :=
|
|
fun x₁ x₂ x₃ x₄ =>
|
|
Expr.eq_of_sort_flat
|
|
{ op := Nat.add, assoc := Nat.add_assoc, comm := Nat.add_comm, vars := [x₁, x₂, x₃, x₄], someVal := x₁ }
|
|
(((Expr.var 0).op (Expr.var 1)).op ((Expr.var 2).op (Expr.var 3)))
|
|
((((Expr.var 2).op (Expr.var 0)).op (Expr.var 1)).op (Expr.var 3)) rfl
|