0 < ε ≤ 0.5 (joke)

Stream: new members

[Eric Wieser]

Edward van de Meent said:

has (hε : 0 < ε ≤ 0.5) ever been valid notation? i don't think so, right?

import Mathlib

instance : OfScientific Prop where
  ofScientific m s e :=
    let q : ℚ := OfScientific.ofScientific m s e
    if q ≤ 0 then
      False
    else if 1 ≤ q then
      True
    else
      Nat = Int


-- `≤ 0.5` means "at most as true as undecidable"
example (ε : Real) (hε : ε = 0) :
    (0 < ε) ≤ 0.5 := by
  aesop

is close

[Kevin Buzzard]

In 2018, $a<b<c$ would hang Lean 3 if they were real numbers, as my students would sometimes discover; it would get parsed as (a<b)<c and then Lean would hang looking for coercions from Prop to real or real to Prop. I think this was before the real number rewrite.