notation

Stream: lean4

[Dean Young]

How could I define a notation like this:

notation C --> D := Fun C D

It's not quite right I think.

or this:

notation "[" C "," D "]" := Fun C D

[Mario Carneiro]

the second one is mostly correct, you need an => as the error message says:

notation "[" C "," D "]" => Fun C D

[Mario Carneiro]

The first one isn't likely to work because -- is the comment syntax (as the syntax highlighting here indicates)

[Arthur Paulino]

I'm not on my PC right now, but is there a \longrightarrow?

[Arthur Paulino]

Arthur Paulino said:

I'm not on my PC right now, but is there a \longrightarrow?

Just tested it: yes, and it can also be spelled \-->. But it can be confused with the common right arrow

[Dean Young]

Arthur Paulino said:

Arthur Paulino said:

I'm not on my PC right now, but is there a \longrightarrow?

Just tested it: yes, and it can also be spelled \-->. But it can be confused with the common right arrow

oh thanks!