ASCII Representations of the Mathematical Symbols (Rodin User Manual)

From Event-B

1 Atomic Symbols
2 Unary Operators
3 Assignment Operators
4 Binary Operators
5 Multiple Operators
6 Quantifiers
7 Bracketing
8 Typing

The mathematical symbols used in the Event-B mathematical language are Unicode characters, beyond the ASCII subset. These characters are not always easy to input with a regular keyboard. To help users enter these characters, a list of standard input strings have been defined. When any of these strings is entered, it is automatically converted by the user interface to the corresponding Unicode character (i.e., mathematical symbol).

Atomic Symbols

ASCII	Symbol
true	$\mathord {\top }$
false	$\mathord {\bot }$
INT	$\mathord {\mathbb Z}$
NAT	$\mathord {\mathbb N}$
NAT1	$\mathord {\mathbb N_1}$

ASCII	Symbol
BOOL	$\mathord {\mathrm{BOOL}}$
TRUE	$\mathord {\mathrm{TRUE}}$
FALSE	$\mathord {\mathrm{FALSE}}$
{}	$\emptyset$

ASCII	Symbol
prj1	$\prjone$
prj2	$\prjtwo$
id	$\id$

Unary Operators

ASCII	Symbol
not	$\neg$
finite	$\finite$
card	$\card$
POW	$\pow$
POW1	$\pown$

ASCII	Symbol
union	$\union$
inter	$\inter$
dom	$\dom$
ran	$\ran$
~	~

ASCII	Symbol
min	$min$
max	$max$
-	$-$

Assignment Operators

ASCII	Symbol
:=	$\bcmeq$
:	$\bcmsuch$
::	$\bcmin$

Binary Operators

ASCII	Symbol
&	$\land$
or	$\lor$
=>	$\limp$
<=>	$\leqv$
=	$=$
/=	$\neq$
:	$\in$
<<:	$\subset$
/<<:	$\not\subset$
<:	$\subseteq$
/<:	$\not\subseteq$
<	$<$
<=	$\leq$
>	$>$
>=	$\geq$
/:	$\notin$

ASCII	Symbol
\|->	$\mapsto$
<->	$\rel$
<<->	$\trel$
<->>	$\srel$
<<->>	$\strel$
+->	$\pfun$
-->	$\tfun$
+>>	$\psur$
->>	$\tsur$
>->>	$\tbij$
/\	$\binter$
\/	$\bunion$
\	$\setminus$
**	$\cprod$
>->	$\tinj$
>+>	$\pinj$