This is blocked on leanprover-community/lean#784 making its way through the pipeline.
The output, while syntactically correct, is pretty rough:
theorem WellFounded.asymmetric {α : Sort _} {r : α → α → Prop} (h : WellFounded r) : ∀ ⦃a b⦄, r a b → ¬r b a
| a => fun b hab hba => WellFounded.asymmetric hba hab termination_by' ⟨_, h⟩decreasing_by assumption
This will need to be fixed in core though. where clause formatting is also broken in a similar way:
/-- The characteristic of the product of rings is the least common multiple of the
characteristics of the two rings. -/
instance [CharP S q] :
CharP (R × S)
(Nat.lcm p
q) where cast_eq_zero_iff := by
simp [Prod.ext_iff, CharP.cast_eq_zero_iff R p, CharP.cast_eq_zero_iff S q, Nat.lcm_dvd_iff]
This is blocked on leanprover-community/lean#784 making its way through the pipeline.
The output, while syntactically correct, is pretty rough:
This will need to be fixed in core though.
whereclause formatting is also broken in a similar way: