Zulip Chat Archive

Stream: general

Topic: linter bail?


Johan Commelin (Jun 23 2021 at 18:26):

#lint-
/- The `ge_or_gt` linter reports: -/
/- The following declarations use ≥/>, probably in a way where we would prefer
  to use ≤/< instead. See note [nolint_ge] for more information. -/
#print Mbar_bdd.transition_eq /- the type contains ≥/>. Use ≤/< instead. -/

#print Mbar_bdd.transition_eq
----
@[_refl_lemma]
theorem Mbar_bdd.transition_eq :  {r' : 0} {S : Fintype} {c : 0} {M N : } (h : M  N) (F : Mbar_bdd r' S c N) (s : S)
(i : fin (M + 1)), (Mbar_bdd.transition r' h F).to_fun s i = F.to_fun s ((fin.cast_le _) i) :=
λ {r' : 0} {S : Fintype} {c : 0} {M N : } (h : M  N) (F : Mbar_bdd r' S c N) (s : S)
(i : fin (M + 1)), rfl

Johan Commelin (Jun 23 2021 at 18:26):

(This is from LTE)

Kevin Buzzard (Jun 23 2021 at 22:25):

What does it look like with pp.all on?


Last updated: Dec 20 2023 at 11:08 UTC