Zulip Chat Archive

Stream: new members

Topic: Notation


Alex Zhang (Jun 01 2021 at 09:02):

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 (Jun 01 2021 at 09:06):

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 (Jun 01 2021 at 09:07):

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


Last updated: Dec 20 2023 at 11:08 UTC