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

chore: fix parenthesizing in test

Browse source
This commit is contained in:
arthur-adjedj 2024-06-29 16:19:22 +02:00 • committed by Kim Morrison
parent 642c28cdbb
commit 93ac635a89
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Init/Data/Nat/Linear.lean
View file

@ -173,13 +173,13 @@ instance : LawfulBEq PolyCnstr where
eq_of_beq {a b} h := by
cases a; rename_i eq₁ lhs₁ rhs₁
cases b; rename_i eq₂ lhs₂ rhs₂
have h : eq₁ == eq₂ && lhs₁ == lhs₂ && rhs₁ == rhs₂ := h
have h : eq₁ == eq₂ && (lhs₁ == lhs₂ && rhs₁ == rhs₂) := h
simp at h
have ⟨⟨h₁, h₂⟩, h₃⟩ := h
have ⟨h₁, h₂, h₃⟩ := h
rw [h₁, h₂, h₃]
rfl {a} := by
cases a; rename_i eq lhs rhs
show (eq == eq && lhs == lhs && rhs == rhs) = true
show (eq == eq && (lhs == lhs && rhs == rhs)) = true
simp [LawfulBEq.rfl]
def PolyCnstr.mul (k : Nat) (c : PolyCnstr) : PolyCnstr :=