Notation

Stream: new members

[Alex Zhang]

import data.real.basic

def converges_to (s : ℕ → ℝ) (a : ℝ) :=
∀ ε > 0, ∃ N, ∀ n ≥ N, abs (s n - a) < ε

If I want to use a predicate as an infix predicate or use a new symbol to denote it, what should do? (taking the above predicate "converges_to" as an example)

[Horatiu Cheval]

import data.real.basic

def converges_to (s : ℕ → ℝ) (a : ℝ) :=
∀ ε > 0, ∃ N, ∀ n ≥ N, abs (s n - a) < ε

infixl `↣` : 30 := converges_to

example (s : ℕ → ℝ) (a : ℝ) : s ↣ a := sorry

[Horatiu Cheval]

You can use infixl or infixr depending on the associativity you want from your infix. The number after the colon is the precedence