Rodin Keyboard User Guide

Introduction

This short help page provides necessary information on the Rodin Keyboard plug-in and also on how to extend the plug-in.

Getting Started

Overview

The Rodin Keyboard plug-in creates a view (namely "RODIN Keyboard") under Event-B category.

You can open "RODIN Keyboard" view now:

1. Go to Window/Show View/Other.
2. Choose the "RODIN Keyboard" view from the Event-B category.

The view contains a text area which takes an ASCII input and translate it into the mathematical language (defined by extensions).

Special Combos

Below are the special combos (set of ASCII characters) and their translations into the Event-B mathematical language.

ASCII	LaTeX	Math	Meaning	Unicode
NAT	\nat	$\nat$	The set of natural numbers	U+2115
NAT1	\natn	$\natn$	The set of positive natural numbers	U+2115 U+0031
INT	\intg	$\intg$	The set of integer numbers	U+2124
POW	\pow	$\pow$	The set of all subsets (power set)	U+2119
POW1	\pown	$\pown$	The set of all non-empty subsets	U+2119 U+0031
(	(	(	Left parenthesis	U+0028
)	)	)	Right parenthesis	U+0029
<=>	\leqv	$\leqv$	Logical equivalence	U+21D4
=>	\limp	$\limp$	Logical implication	U+21D2
&	\land	$\land$	Logical conjunction	U+2227
or	\lor	$\lor$	Logical disjunction	U+2228
not	\lnot	$\lnot$	Not sign	U+00AC
true	\btrue	$\btrue$	True predicate	U+22A4
false	\bfalse	$\bfalse$	False predicate	U+22A5
!	\forall	$\forall$	For all	U+2200
#	\exists	$\exists$	There exists	U+2203
,	,	,	Comma	U+002C
.	\qdot	$\qdot$	Middle dot	U+00B7
=	=	=	Equal to	U+003D
/=	\neq	$\neq$	Not equal to	U+2260
<	<	<	Less than	U+003C
<=	\leq	$\leq$	Less than or equal to	U+2264
>	>	>	Greater than	U+003E
>=	\geq	$\geq$	Greater than or equal to	U+2265
:	\in	$\in$	Element of	U+2208
/:	\notin	$\notin$	Not an element of	U+2209
<<:	\subset	$\subset$	(Proper) Subset of	U+2282
/<<:	\notsubset	$\not\subset$	Not a (proper) subset of	U+2284
<:	\subseteq	$\subseteq$	Subset of or equal to	U+2286
/<:	\notsubseteq	$\not\subseteq$	Neither a subset of nor equal to	U+2288
<->	\rel	$\rel$	Relation	U+2194
<<->	\trel	$\trel$	Total relation	U+E100
<->>	\srel	$\srel$	Surjective relation	U+E101
<<->>	\strel	$\strel$	Total surjective relation	U+E102
+->	\pfun	$\pfun$	Partial function	U+21F8
-->	\tfun	$\tfun$	Total function	U+2192
>+>	\pinj	$\pinj$	Partial injection	U+2914
>->	\tinj	$\tinj$	Total injection	U+21A3
+>>	\psur	$\psur$	Partial surjection	U+2900
->>	\tsur	$\tsur$	Total surjection	U+21A0
>->>	\tbij	$\tbij$	Bijection	U+2916
{	{	{	Left curly bracket	U+007B
}	}	}	Right curly bracket	U+007D
->	\mapsto	$\mapsto$	Maplet	U+21A6
,,
{}	\emptyset	$\emptyset$	Empty set	U+2205
/\	\binter	$\binter$	Intersection	U+2229
\/	\bunion	$\bunion$	Union	U+222A
\	\setminus	$\setminus$	Set minus	U+2216
**	\cprod	$\cprod$	Cartesian product	U+00D7
[	[	[	Left square bracket	U+005B
]	]	]	Right square bracket	U+005D
<+	\ovl	$\ovl$	Relation overriding	U+E103
circ	\bcomp	$\bcomp$	Backward composition	U+2218
;	\fcomp	$\fcomp$	Forward composition	U+003B
><	\dprod	$\dprod$	Direct product	U+2297
||	\pprod	$\pprod$	Parallel product	U+2225
~	\conv	~	Tilde operator	U+223C
<|	\domres	$\domres$	Domain restriction	U+25C1
<<|	\domsub	$\domsub$	Domain subtraction	U+2A64
>	\ranres	$\ranres$	Range restriction	U+25B7
>>	\ransub	$\ransub$	Range subtraction	U+2A65
%	\lambda	$\lambda$	Lambda	U+03BB
INTER	\Inter	$\Inter$	N-ary intersection	U+22C2
UNION	\Union	$\Union$	N-ary union	U+22C3
|	\mid	$\mid$	Such that	U+2223
..	\upto	$\upto$	Upto sign	U+2025
+	+	+	Addition sign	U+002B
-	-	-	Subtraction sign	U+2212
*	*	*	Multiplication sign	U+2217
/	\div	$\div$	Division sign	U+00F7
^	\expn	$\expn$	Exponentiation sign	U+005E
oftype	\oftype	File:Oftype	Typing operator	U+2982
:=	\bcmeq	$\bcmeq$	Becomes equal to	U+2254
::	\bcmin	$\bcmin$	Becomes an element of	U+003A U+2208
:|	\bcmsuch	$\bcmsuch$	Becomes such that	U+003A U+2223